Live data from Hacker News

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

ralfj.de

91–100 of 135 posts

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

#91
Thinking about this quite a bit, I see the second optimization as pretty obviously incorrect - not because of provenance, but because it acts as if pointer-to-integer-to-pointer casting is value-preserving, which is not at all guaranteed by the C abstract machine. In particular, `p != q && ((uintptr_t)p == (uintptr_t)q)` can be true according to the C standard. Instead of trying to track provenance, simply considering that the transformation between pointers and integers is not value preserving seems to be a simpler rule.

If we want to reason about optimizations using the C abstract machine, we can't consider these transformations to be value-preserving, even if they happen to be in the real machines that LLVM targets (and if they start reasoning for the real machine instead of the C abstract machine, a lot of other optimizations are invalid).

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

#92
I think that the main problem is that pointers are a too low-level concept (like assembly language compared to high-level programming languages) that are used to implement various more high-level concepts. I have not come across a language that does have pointers (some functional languages lack pointers all together) and has these high-level concepts. There is a great difference between a pointer that points to a complex value and a pointer, that like a database cursor, points to a certain part in a complex value, either with the purpose to query this value or to make some change to the value.

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

#94
post #9

Earlier quoted context omitted.

It’s enough of an issue for C at least that a fully formally verified compiler exists: https://en.m.wikipedia.org/wiki/CompCert . That is, there’s proof that its (limited) optimisation passes are correct. There’s other approaches to assurance of compiled code too, such as seL4 which has proofs that the binary itself is correct, I believe.

Note that fuzzing CompCert has still found bugs in it - because the entire compiler actually isn't verified. They've extended the proof over time. (Note that "formally verified" still does not mean "bug free", it just means it's a refinement of a proof that is also a program which can have bugs in it. And "formally" sounds like a weasel word.)

Ah, thanks for the clarification!

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

#95
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…

That's impossible in the general case, since it's trivially equivalent to the halting problem (take the UB-detecting compiler, have it perform UB iff the program has no UB, run it on its own source code).

What we can do is a combination of formal methods, heuristics and sanitizers. Plus software engineering techniques, such as running tests to high coverage with sanitizers, fuzzing, and so on.

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

#96
post #21

Earlier quoted context omitted.

As usual; if a compiler knows about undefined behavior I would much rather it throw an error rather than optimize something the programmer didn't intend based on the compiler out-smarting a human's ability to be specific.

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…

For your first example, I think most people want integer overflow to be unspecified behavior instead of undefined behavior - this is how most other languages treat it, it is how all C compilers behaved for a long time, and it is unreasonably difficult to actually write C code that makes sure not to cause integer overflow.

Your example is in fact perfect for why that should be the case: consider the following code:

  int n = 0;
  scanf("%d", &n)
  factorial(n); //using your definition of factorial(int)
A standard-compliant C compiler is apparently free to optimize this program to format your hard-drive.

For your second example, I would say that, rather than omitting the NULL check, a helpful compiler could do one of two things:

1. Don't reason from strlen(s) to s != NULL, so the NULL check must be left in (unless it has even more context and can see a non-NULL assignment to s) 2. Wherever trying to optimize away a comparison to NULL based on UB reasoning, put in a new comparison to NULL at the place you applied that reasoning. For this example, optimize the program as if it looked like this:

  //first, the inline version  
  void puts_with_len(const char *s) {
    s_len = strlen(s);
    printf("len = %zu\n", s_len);
    const char* puts_arg = s == NULL ? "(null)" : s
    puts(puts_arg)
  }
  //after optimization
  void puts_with_len(const char *s) {
    s_len = strlen(s);
    const char* puts_arg;
    if (s != NULL) {
      puts_arg = s;
    } else {
      puts_arg = "(null)"; //could also explicitly signal a segfault or assert here instead
    }
    printf("len = %zu\n", s_len);    
    puts(puts_arg);
  }
In this case we didn't gain anything, but if puts_with_len were itself inlined the check would be moved further back, potentially replacing many NULL checks with a single one.

I would note that there is a third option here that goes in a different direction: now that compilers are extremely aggressive with NULL check removal optimizations, a lot of unsafe C functions could be made safe by manually adding the missing NULL checks to the stdlib and other major libraries. This wouldn't affect the semantics, and it wouldn't hurt performance assuming the optimizer really is doing its business.

For example, strlen() could itself raise an assertion/exit on strlen(NULL). If called from a context where it is known that s != NULL, the null check can be optimized away by the aggressive optimizer; if not, better safe than sorry.

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

#97
For purposes of future language design: why not just ban conversion from integers to pointers? Pointers have metadata that integers can't provide, therefore the conversion is impossible, QED. What's the use case for it outside of, say, binary executable loaders?

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

#98
post #82

Earlier quoted context omitted.

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 t…

> 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()".

This is really a question of how the semantics are formulated. The eval function I gave doesn't take into account an abstract machine so there is no notion of "variable allocation" or "final state" to check, the semantics doesn't account for it.

To scale it to a more realistic model with nondeterminism, heaps and so on, the semantics needs to be changed to a relational one. For instance, eval would now be a relation that relates two states of the machine, and a proof of correctness would be something like[0], which takes into account all possible states of the heap.

Equality would no longer used to relate two "equivalent" programs but rather some other equivalence relation with the properties one cares about, for instance two programs would be heap-equivalent if they have exactly the same effect on the heap, or UB-equivalent if they have possible UB at the "same" (again under another relation) places.

[0] https://softwarefoundations.cis.upenn.edu/plf-current/Equiv....

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

#99
post #65

Earlier quoted context omitted.

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…

This is untenable in the general case. For example, consider this function: int dereference(int *p) { return *p; } What should the compiler do in this case? If I pass (int *)0x1283412 into this function, that's undefined behavior…should it just always warn?

The compiler isn't __changing any programmer dictated behavior__. There are no UB sourced 'optimizations' being implicitly disabled and none have been expressly enabled. As long as valid code compiles it's on the humans that wrote the code (or that triggered it's writing in some higher level synthesis tool).

Expanding on this; I don't want compilers _making_ optimizations based on UB. I want them educating the programmers so that the UB can be eliminated at a human level and correct outcomes are the result, optimized if it makes sense.

Post reply on HN