4 ms·
> The problem with your interpretation is that it defies causality. The question of whether this is a well-formed C++ program isn't one that can be delayed unti
by LegionMammal978 3y ago
> The problem with your interpretation is that it defies causality. The question of whether this is a well-formed C++ program isn't one that can be delayed until runtime, it either was, or was not, a well-formed C++ program when it was compiled - so if your reading requires that we don't know until runtime then it cannot be a correct reading.
Alas, the same issues with causality arise with the idea of "time-travelling UB". Suppose I write a program that prints a welcome message, reads a number from the standard input, then either exits if it's 0, or causes UB if it's 1. By the rules of the standard, if the implementation could presciently predict at the start of the program that I am about to enter 1, then it could skip the welcome message.
But of course, in the real world, causality is a higher law than the rules in the standard: if there's a possibility at any point that UB might not occur, then it must keep functioning as expected. So there's no way it can skip the welcome message, even though the standard allows it.
I see the question of ill-formedness from invalid terms as the same. At the start of each execution of the program, each type that must satisfy a requirement gets an invisible "set of valid terms" with respect to that requirement. However, this set exists only in the mathematical sense, in that it cannot yet be known by anyone, since it depends on future information. This is just like "the number that I will eventually enter" in my last example: it mathematically has some value (assuming that I do eventually enter something), but neither I nor the implementation can know whether it's 0 or 1 until I actually enter it.
Thus, the implementation is once again bound by the possibility that the "set of valid terms" might truly satisfy the requirement. It must execute the program as if it is well-formed, right up until the point where it is no longer possible that it is well-formed. And that point will generally correspond to a particular witness value (e.g., a NaN) that is passed into a standard function but makes an operation fail to meet its requirements.
If you want to put it into properly-causal terms, you could start the program with a really big "set of possible sets of valid terms". Then, each time at runtime that the program passes a value to a function with the requirement, you filter the sets to only those containing the value. If there are no sets left after this, then the program is now known for certain to have been ill-formed all along (there's no possibility remaining), so you can do whatever you want.
Of course, this does assume that a program being well-formed can change between each execution, even with the same source file. But it's hardly the only IFNDR in the standard that depends on behavior rather than syntax.
> The other option (which I happen to think is the only reasonable choice) is the one Rust took - only programs which we can show have the desired semantic properties will compile, other programs are rejected. This means the compiler will reject some correct programs, which is somewhat annoying if it happens to you, but effort put into the compiler can reduce the frequency of its occurrence (and it did in Rust, that's what the Non-Lexical Lifetimes change was and what Polonius is all about)
Since you mention Rust, I'd note that it has the same causality wackiness, just to a far lesser extent than C/C++, in the form of "angelic nondeterminism" (which is a term you can Google). Suppose that you have a pointer to the end of one slice and a pointer to the start of another slice, which happen to be equal, but don't have access to each other's slices due to provenance. Then, you convert both those pointers to integers, and convert that integer value back to a pointer.
Which slice should the new pointer have access to? Since integers have no provenance, the compiler has no way of knowing which pointer the address came from! Thus, the compiler uses "angelic nondeterminism" to decide: defying causality, it picks whichever of the two slices will make the program valid. If neither choice is valid (e.g., the program tries to access both slices from the new pointer), then it's instant UB.
Once again, to do this in the real world, the compiler must maintain a conceptual set of possible pointers that the new pointer might have come from, then whittle them down based on what memory is actually accessed. If there are no possible pointers left, then UB is known.
- tialaramex 3y ago> Of course, this does assume that a program being well-formed can change between each execution Which can't be right. > has the same causality wackiness, just to a far lesser extent than C/C++, in the form of "angelic nondeterminism" It's OK, I don't need to Google, you'll find me in a conversation with Martin Uecker in a previous HN thread about PNVI-ae-udi which is the way C or C++ people would think about the matter. And actually as usual Rust is ahead of the game here, you say "the compiler has no way of knowing" - actually with Aria's experiment in play we can insist on always telling the compiler what's going on, and as a reward we get both more assurance of correctness because the tools work (Miri for example) and better performance. The experiment is about whether most Rust software can live with this restriction ("Strict Provenance") and the answer IMNSHO is clearly yes. Rust's pointers get to have member functions (as do its primitive integers and any other types) and Aria's experiment adds the method with_addr() to pointers, so now we can tell a pointer (which has provenance) that we want a different pointer with a different address inside it (but preserving the provenance) via the method. More pertinently to our discussion, even with PNVI-ae-udi plus a mistake that results in an impossible pointer this is a cause of Undefined Behaviour, which occurs at runtime, it is not a semantic requirement of the language, our Rust program was well formed and correctly translated into machine code if we did this wrong, it's just that it had Undefined Behaviour at runtime as a result of us writing bad unsafe code. Because Rust defaults to rejecting programs it knows always panic there can be the false impression that such programs are not well-formed. You can just insist to the compiler that you want the results anyway, it will duly spit out an executable which... always panics. Not sure what you want that for, but you're welcome to it.
- gpderetta 3y agoA well-formed C++ program is one that is "[...] constructed according to the syntax and semantic rules" (4.65). And of course adherence to many semantic rules in C++ cannot generally be verified statically: "A conforming implementation executing a well-formed program shall produce the same observable behavior as one of the possible executions of the corresponding instance of the abstract machine with the same program and the same input. However, if any such execution contains an undefined operation, this document places no requirement on the implementation executing that program with that input (not even with regard to operations preceding the first undefined operation)." (4.1.2.5). It sucks but that's the way C++ work, and it would be hard for it to be any other way without GC or going full rust.