3 ms·

Nah, thanks to CompCert[1] C actually has one of the highest quality and most predictable compilers. [1] https://compcert.org/ https://compcert.org/

by User23 3y ago

Ygg2 3y ago
How much of available C libraries are CompCert compatible?
insanitybit 3y ago
What is the practicality of actually using CompCert? And what does it actually defend against? All I know is that it tries to ensure that the behavior of the program is the same as the input, meaning that the compiler itself does not have bugs. But how does that actually interact with undefined behavior in the language? What happens to an array out of bounds? And what are the limitations imposed, since it only works on a subset of the C language? It seems unlikely that I could just switch compilers and suddenly have a safe program written in C.
- LegionMammal978 3y ago
  It looks like CompCert explicitly does not attempt to prevent UB from resulting in unpredictable behavior; all it guarantees is that "the observable behavior of [the compiled code] C improves on one of the allowed observable behaviors of [the source program] S", where "improving on" allows for arbitrary behavior on UB [0]: > Third, the compiler is allowed to improve the behavior of the source program. Here, to improve means to convert a run-time error (such as crashing on an integer division by zero) into a more defined behavior. This can happen if the run-time error (e.g. division by zero) was optimized away (e.g. removed because the result of the division is unused). However, if the source program is known to be free of run-time errors, perhaps because it was verified using static analyzers or deductive program provers, improvement as described above never takes place, and the generated code behaves exactly as one of the allowed behaviors of the source program. So you still have to prove your program's correctness by some other means. [0] https://compcert.org/man/manual001.html#sec3 https://compcert.org/man/manual001.html#sec3
  - User23 3y ago
    You have to scroll down a bit, but see here[1]. Also searching [site:regehr.org compcert] will find more. CompCert C makes it impossible to reproduce at least some UB bugs: For CompCert, the high-level correctness theorems I proved are all of the first kind above: if the source program goes wrong, nothing is guaranteed about the behavior of the compiled code. It happens, however, that the stepwise simulation lemmas I build on actually prove property 2 above: the compiled code cannot crash "earlier" than the source code, and will produce the same pre-crash observables, then possibly more. So maybe I should strengthen my high-level correctness theorems... That was over a decade ago, so perhaps it's been done. I confess I haven't closely followed CompCert in some time, due to having priorities elsewhere. As you can see elsewhere in that reference CompCert C will fail to generate the example UB code. But yes, mechanically proving additional properties with some kind of SAT solver is also an open area of research. Dafny is the example I’m familiar with. Its conditions and invariants allow things like automatically proved binary search[2]. Converting CompCert C statements to SMTLibv2 assertions (which is, to an extremely rough first approximation what Dafny does) would certainly be considerably easier than it would be for most other languages. It would still be a serious effort of course. [1] https://blog.regehr.org/archives/232 https://blog.regehr.org/archives/232 [2] https://github.com/dafny-lang/dafny/blob/master/Test/dafny4/BinarySearch.dfy https://github.com/dafny-lang/dafny/blob/master/Test/dafny4/...
    - LegionMammal978 3y ago
      Apart from compiler bugs, this issue with "time-traveling UB" shouldn't really occur in practice with any side effects other than volatile accesses. As noted by Martin Uecker [0], > In portable C code I/O is performed using function calls of the standard library. A compiler can generally not assume that a function returns to the caller, because the function could call ‘exit’, ‘abort’, ‘longjmp’, or enter an infinite loop. For this reason, it is never allowed for a compiler to use any information derived from an operation with potential UB that comes after a function call in a way that could affect observable behavior before the function call. Consequently, observable behavior that is accessed via function calls (i.e. all except volatile accesses) can not be affected by time-traveling optimizations even when using the abstract interpretation. In principle, a compiler could use special knowledge about C library functions and use the fact those functions always return to the caller, but we are not aware of any compiler which does this (and it hardly seems worthwhile). I believe LLVM has a "mustreturn" attribute expressing this, but as noted, no standard C library messes with any such attributes for functions that cause observable behavior. So time-traveling UB really only affects programs which use volatile accesses for MMIO, and it might eventually be banned entirely from the C standard if the linked proposal N3128 goes through. I'd say that even "some C bugs" is a overstatement outside of embedded programming, given the rarity of MMIO in a hosted environment. [0] https://www.open-std.org/jtc1/sc22/wg14/www/docs/n3128.pdf https://www.open-std.org/jtc1/sc22/wg14/www/docs/n3128.pdf
eru 3y ago
Well, that one tells you that the compilers translate your program according to the language spec. That's helpful, but doesn't make the language itself saner.

Nah, thanks to CompCert[1] C actually has one of the highest quality and most predictable compilers. [1] https://compcert.org/ https://compcert.org/

by User23 3y ago

Nah, thanks to CompCert[1] C actually has one of the highest quality and most predictable compilers. [1] https://compcert.org/ https://compcert.org/

Ygg2 3y ago

How much of available C libraries are CompCert compatible?

insanitybit 3y ago

What is the practicality of actually using CompCert? And what does it actually defend against? All I know is that it tries to ensure that the behavior of the program is the same as the input, meaning that the compiler itself does not have bugs. But how does that actually interact with undefined behavior in the language? What happens to an array out of bounds? And what are the limitations imposed, since it only works on a subset of the C language? It seems unlikely that I could just switch compilers and suddenly have a safe program written in C.

LegionMammal978 3y ago
It looks like CompCert explicitly does not attempt to prevent UB from resulting in unpredictable behavior; all it guarantees is that "the observable behavior of [the compiled code] C improves on one of the allowed observable behaviors of [the source program] S", where "improving on" allows for arbitrary behavior on UB [0]: > Third, the compiler is allowed to improve the behavior of the source program. Here, to improve means to convert a run-time error (such as crashing on an integer division by zero) into a more defined behavior. This can happen if the run-time error (e.g. division by zero) was optimized away (e.g. removed because the result of the division is unused). However, if the source program is known to be free of run-time errors, perhaps because it was verified using static analyzers or deductive program provers, improvement as described above never takes place, and the generated code behaves exactly as one of the allowed behaviors of the source program. So you still have to prove your program's correctness by some other means. [0] https://compcert.org/man/manual001.html#sec3 https://compcert.org/man/manual001.html#sec3
- User23 3y ago
  You have to scroll down a bit, but see here[1]. Also searching [site:regehr.org compcert] will find more. CompCert C makes it impossible to reproduce at least some UB bugs: For CompCert, the high-level correctness theorems I proved are all of the first kind above: if the source program goes wrong, nothing is guaranteed about the behavior of the compiled code. It happens, however, that the stepwise simulation lemmas I build on actually prove property 2 above: the compiled code cannot crash "earlier" than the source code, and will produce the same pre-crash observables, then possibly more. So maybe I should strengthen my high-level correctness theorems... That was over a decade ago, so perhaps it's been done. I confess I haven't closely followed CompCert in some time, due to having priorities elsewhere. As you can see elsewhere in that reference CompCert C will fail to generate the example UB code. But yes, mechanically proving additional properties with some kind of SAT solver is also an open area of research. Dafny is the example I’m familiar with. Its conditions and invariants allow things like automatically proved binary search[2]. Converting CompCert C statements to SMTLibv2 assertions (which is, to an extremely rough first approximation what Dafny does) would certainly be considerably easier than it would be for most other languages. It would still be a serious effort of course. [1] https://blog.regehr.org/archives/232 https://blog.regehr.org/archives/232 [2] https://github.com/dafny-lang/dafny/blob/master/Test/dafny4/BinarySearch.dfy https://github.com/dafny-lang/dafny/blob/master/Test/dafny4/...
  - LegionMammal978 3y ago
    Apart from compiler bugs, this issue with "time-traveling UB" shouldn't really occur in practice with any side effects other than volatile accesses. As noted by Martin Uecker [0], > In portable C code I/O is performed using function calls of the standard library. A compiler can generally not assume that a function returns to the caller, because the function could call ‘exit’, ‘abort’, ‘longjmp’, or enter an infinite loop. For this reason, it is never allowed for a compiler to use any information derived from an operation with potential UB that comes after a function call in a way that could affect observable behavior before the function call. Consequently, observable behavior that is accessed via function calls (i.e. all except volatile accesses) can not be affected by time-traveling optimizations even when using the abstract interpretation. In principle, a compiler could use special knowledge about C library functions and use the fact those functions always return to the caller, but we are not aware of any compiler which does this (and it hardly seems worthwhile). I believe LLVM has a "mustreturn" attribute expressing this, but as noted, no standard C library messes with any such attributes for functions that cause observable behavior. So time-traveling UB really only affects programs which use volatile accesses for MMIO, and it might eventually be banned entirely from the C standard if the linked proposal N3128 goes through. I'd say that even "some C bugs" is a overstatement outside of embedded programming, given the rarity of MMIO in a hosted environment. [0] https://www.open-std.org/jtc1/sc22/wg14/www/docs/n3128.pdf https://www.open-std.org/jtc1/sc22/wg14/www/docs/n3128.pdf

eru 3y ago

Well, that one tells you that the compilers translate your program according to the language spec. That's helpful, but doesn't make the language itself saner.