Live data from Hacker News

Pointers Are Complicated II, or: We need better language specs

ralfj.de

81–90 of 135 posts

Re: Pointers Are Complicated II, or: We need better language specs

#81
post #79

Earlier quoted context omitted.

> Just because two pointers point to the same memory location, it does not mean they have an identical representation as an integer. Yes, I know. That's irrelevant here for two reasons: firstly, the pointers might compare equal (which is all that matters for this argument), and secondly, once again, the comparison isn't being made between pointers , the comparison is being made between integers. > The entire page is…

> Yes, I know. That's irrelevant here for two reasons: firstly, the pointers might compare equal (which is all that matters for this argument), and secondly, once again, the comparison isn't being made between pointers, the comparison is being made between integers. You know what, I think you're right, at least on the second point. I guess the code isn't UB after all then. Somehow I kept reading it as if it's compari…

> There are multiple entities here, in agreement with each other. The author links to bug #61502 in GCC, where you'll see the compiler devs agree with the author of that page: https://gcc.gnu.org/bugzilla/show_bug.cgi?id=61502#c15

No they don't. The previous comment from that compiler dev explicitly says that this comparison is not undefined behaviour. There is nothing in either the standard or that bug report that supports the claim that you originally posted ("Comparing pointers for equality is defined if both pointers are derived from the same (multidimensional) array object. Thus, if two pointers point to different array objects, then these array objects must be subaggregates of the same multidimensional array object in order to compare them. Otherwise this leads to undefined behavior."). Equality comparisons (not relational comparisons) of pointers to (unrelated) arrays are not and never have been undefined behaviour, and anyone claiming they are is at best confused.

Re: Pointers Are Complicated II, or: We need better language specs

#82
post #5

> However, to make the argument that an optimization is correct, the exact semantics of LLVM IR (what the behavior of all possible programs is and when they have UB) needs to be documented. This is a great point as to why formal semantics of programming languages matters. Even if an optimization seems "obviously" correct, finicky things like introducing the possibility of UB can, as the post outlines, cascade into co…

Not sure why you wanted to spend the time to prove "correct optimizations can be combined", but I take issue with that proof. It only works for optimizations that give code exactly the same behavior, which is severely limiting.

Exactly the same as in the as-is rule or optimisations explicitly allowed by the standard?

Re: Pointers Are Complicated II, or: We need better language specs

#83

Earlier quoted context omitted.

If the programmer really needs reads and writes through particular pointers to happen in a particular sequence, because the target memory follows different rules than the language ordinarily allows the compiler to assume, then it’s the programmer’s responsibility to use the annotation provided by the language for exactly that purpose: volatile. If the compiler had to assume that every pointer needs to be treated as v…

To be extra pedantic, that's not what volatile does. Volatile ensures that access through the variable must behave strictly according to the rules of the C abstract machine, but the definition of access is implementation defined . A compiler author could define "access" to be "reads from the variable" or "writes to the variable", or neither, and make the entire keyword useless. As long as they document that somewhere…

> A compiler author could define "access" to be "reads from the variable" or "writes to the variable", or neither, and make the entire keyword useless. As long as they document that somewhere, it's compliant with the standard.

Nobody is going to accept that as a compliant implementation.

Re: Pointers Are Complicated II, or: We need better language specs

#84
post #5

> However, to make the argument that an optimization is correct, the exact semantics of LLVM IR (what the behavior of all possible programs is and when they have UB) needs to be documented. This is a great point as to why formal semantics of programming languages matters. Even if an optimization seems "obviously" correct, finicky things like introducing the possibility of UB can, as the post outlines, cascade into co…

Not sure why you wanted to spend the time to prove "correct optimizations can be combined", but I take issue with that proof. It only works for optimizations that give code exactly the same behavior, which is severely limiting.

That's not a problem in the proof, it's part of the definition of a "correct optimization", given above.

Re: Pointers Are Complicated II, or: We need better language specs

#85
post #82

Earlier quoted context omitted.

Not sure why you wanted to spend the time to prove "correct optimizations can be combined", but I take issue with that proof. It only works for optimizations that give code exactly the same behavior, which is severely limiting.

Exactly the same as in the as-is rule or optimisations explicitly allowed by the standard?

There are two big issues.

One is that the as-is rule only says that code has to match a possible execution of the abstract machine. Let's say an optimization changes the address where a variable gets allocated. That's an extremely valid optimization, even though the program can observe the change. But that would make it fail the "eval e = eval (opt e)" rule in siraben's proof. The same for picking a different order to execute the functions in "f() + g()".

The other is optimizing around undefined behavior. The as-is rule only applies for valid inputs. Optimizing a loop by assuming you won't overflow would get rejected by that proof. So would optimizing code so that it won't segfault.

And depending on how exactly that eval test works, it might effectively mark every variable as volatile too.

Re: Pointers Are Complicated II, or: We need better language specs

#86

Earlier quoted context omitted.

Not sure why you wanted to spend the time to prove "correct optimizations can be combined", but I take issue with that proof. It only works for optimizations that give code exactly the same behavior, which is severely limiting.

That's not a problem in the proof, it's part of the definition of a "correct optimization", given above.

I count the definitions given for a proof as part of the proof.

Re: Pointers Are Complicated II, or: We need better language specs

#87
post #65

Earlier quoted context omitted.

I've heard this proposal thrown around a lot on HN, but how would that even work? Can you describe how the compiler would do this, what patterns it would look for, and what error messages it would produce? For example, consider this: int factorial(int n) { int r = 1; for (int i = 1; i Since there are two instances of possible UB in the above function, what error messages would you like the compiler to produce? First…

What I want is for the compiler to have a mode (which ideally would be enabled by default, at least with modern compile targets) that never optimizes based on undefined behavior. It would do this by handing any UB as an error and making the programmer write a correct program that lacks UB through informing the programmer where undefined behavior has been proven by the compiler. This would improve both the code and th…

One challenge is that there are lots of cases where a program might have UB for a certain input, but a full-program analysis reveals that this UB is not actually possible to hit with any execution.

Should it still report UB? What if the full program analysis is beyond what the compiler is able to reason about?

Re: Pointers Are Complicated II, or: We need better language specs

#88

Earlier quoted context omitted.

That's not a problem in the proof, it's part of the definition of a "correct optimization", given above.

I count the definitions given for a proof as part of the proof.

That is a serious mistake here, where the definition of a correct optimization is of significantly more interest than the result that they can be composed. We want to apply optimizations alone even more than we want to apply them together.

Putting things another way, this definition is clearly not given as part of a proof; it is given for its own sake, and the proof uses it.

Re: Pointers Are Complicated II, or: We need better language specs

#89

Earlier quoted context omitted.

I count the definitions given for a proof as part of the proof.

That is a serious mistake here, where the definition of a correct optimization is of significantly more interest than the result that they can be composed. We want to apply optimizations alone even more than we want to apply them together. Putting things another way, this definition is clearly not given as part of a proof; it is given for its own sake, and the proof uses it.

I wouldn't call slightly imprecise wording a "serious mistake".

I object to points at the part of the post. My objections are unchanged by what we call it.

Re: Pointers Are Complicated II, or: We need better language specs

#90
post #66

Earlier quoted context omitted.

> In LLVM this might just be a weird side-effect we don't care about, but actually having an integer overflow is a big deal in C that introduces UB. Given the introduction, LLVM (incorrectly) introduces (C) UB at times. This doesn't matter. LLVM IR is not C, and it is not convertible to C, as it implements a superset of C semantics, which includes some cases where behavior that is undefined in C is well-defined in LL…

> This doesn't matter. Maybe I expressed myself a bit too literally, but I wouldn't say that how LLVM handles UB "doesn't matter." Look at how Clang compiles undefined behavior vs GCC (for example)[1]. A bit tautological, but different ways of handling UB can lead to different ways UB behaves. > LLVM IR is not C, and it is not convertible to C... This isn't strictly true. There used to be an "official" C(pp) backend,…

> different ways of handling UB can lead to different ways UB behaves.

Ha! If something depends on how 'undefined behavior' behaves, then it's not really undefined, is it? :D

Post reply on HN