3 ms·
You have to choose whether or not you want the compiler to generate code that spends time doing things that the programmer didn't ask for. If you write a libra
by xamuel 11y ago
You have to choose whether or not you want the compiler to generate code that spends time doing things that the programmer didn't ask for.
If you write a library with a function which accepts variables x and y and computes x[y] (or x<<y), there's no way for the compiler to know in advance whether the user will pass in well-behaved values for x and y. If you insist on the behavior being defined in pathological cases, then the compiler must add some kind of branching logic in there to check what's passed in at runtime. In other words, spend time doing things the programmer didn't ask for.
Maybe when we make more progress with formal proof-generating languages, we can create a "friendly" C where the compiler refuses to compile the code until it's accompanied by formal proofs of UB-avoidance.
- Animats 11y ago"Maybe when we make more progress with formal proof-generating languages, we can create a "friendly" C where the compiler refuses to compile the code until it's accompanied by formal proofs of UB-avoidance." That's entirely feasible. I headed a team which did that for a dialect of Pascal over three decades ago.[1] It's since been done for Modula III, Java, Spec#, and Microsoft Windows drivers. One reasonable thing to do is to have the compiler generate run-time assertions for every statement which has a precondition for defined behavior. All pointer dereferences get "assert(p != 0)". The shift problem in the original article gets "assert(n > 0); assert(n <= 32);" Now everything has run-time checks. Then you try to optimize out the run-time checks, or at least hoist them out of loops. A simple prover can remove about 90% of the checks without much effort. [1] http://www.animats.com/papers/verifier/verifiermanual.pdf http://www.animats.com/papers/verifier/verifiermanual.pdf