Timeline for How could I implement a non-null pointer qualifier in a C-style language?
Current License: CC BY-SA 4.0
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 7, 2023 at 1:06 | vote | accept | CPlus | ||
| S May 23, 2023 at 11:14 | history | suggested | springogeek | CC BY-SA 4.0 |
Correcting spelling in the title
|
| May 23, 2023 at 9:38 | review | Suggested edits | |||
| S May 23, 2023 at 11:14 | |||||
| May 23, 2023 at 1:45 | comment | added | Ray Butterworth |
"if a pointer qualified with nonnull contains NULL and is read, immediate undefined behavior is invoked" — so a valid implementation of the nonnull attribute would be to simply ignore it? Put `#define nonnull' at the top of any source, and you've already got what you asked for with all existing compilers. Or am I missing something?
|
|
| May 23, 2023 at 1:04 | answer | added | Longinus | timeline score: 5 | |
| May 22, 2023 at 21:52 | comment | added | chrysante | That's an interesting perspective on the topic. I only ever thought about type checking as a peephole analysis, i.e. when you encounter an int to string assignment you reject it regardless of the context. But still the idea of rejecting valid programs makes me feel uneasy somehow. But then again I had never considered your example with Fermats theorem as a valid program that I would cry over if it gets rejected, but technically it is valid of course. | |
| May 22, 2023 at 21:42 | comment | added | kaya3 |
Even so, the halting problem is rarely relevant for compilers; all non-trivial static analyses (including type safety, definite assignment, and so on) can be reduced to the halting problem if the compiler must accept all valid programs and reject all invalid programs. In practice this just means compilers are written to accept most valid programs, and reject all invalid and some valid programs. For intuition, imagine a program which assigns 23 to a string variable if it finds a counterexample to Fermat's last theorem; this program is type-safe, but all real type-checkers reject it.
|
|
| May 22, 2023 at 21:35 | comment | added | kaya3 | @chrysante In Typescript, if the check is performed by a function then the function can be labelled as a type predicate. Typescript doesn't check the validity of type predicate functions, but the same logic used for narrowing could be used to do this (or if you're C, you could just not check them, and make it UB if a type predicate returns true when the argument doesn't satisfy the type it's supposed to check for). The goal is not to validate as many valid programs as possible, the goal is to give the programmer enough tools that it's not hard to write in a way the compiler can validate. | |
| May 22, 2023 at 21:31 | comment | added | chrysante | @kaya3 Thank you, that is indeed interesting. But constructing a breaking example seems very trivial, especially since OP is implementing a C-like language where you can probably insulate code in different translation units. If the null pointer check is in a function that the compiler can't analyze it can only reject the code. I have no idea how code insulation in type script works or if it even exists but in a C-like language I feel like this would be a problem | |
| May 22, 2023 at 21:18 | comment | added | kaya3 | @chrysante Typescript is a notable example. In almost all real cases, there is no issue, and when there is it's usually straightforward to rewrite the code in a way that the compiler can recognise as valid. The documentation lists exactly the conditions which can be used to narrow nullable types, so as long as your access is guarded by one of those conditions then you're fine. | |
| May 22, 2023 at 21:13 | comment | added | chrysante | @kaya3 May I ask which languages implement such conservative control flow proofs? I'm genuinely curious, but it seems like it would be very unsatisfying to have the compiler reject perfectly valid programs because it's not able to proof their safety. | |
| May 22, 2023 at 20:53 | comment | added | CPlus | @kaya3 There has to be a better way than control-flow analysis. | |
| May 22, 2023 at 20:50 | comment | added | kaya3 | Checking at compile-time is absolutely possible, you just check conservatively and reject programs which aren't provably safe. Whenever someone invokes the halting problem to argue something is impossible, there are a hundred languages already doing it. In this case, there are two general approaches ─ control-flow type narrowing when the pointer is checked in a conditional branch (this is basically OP's suggestion), or having an option type with an API for safe access. | |
| May 22, 2023 at 20:27 | comment | added | chrysante |
You could make it some sort of explicit cast and say that casting a null pointer to a nonnull is UB. Then your compiler can implement a runtime check. But checking at compile time is (afaik) not possible in general
|
|
| May 22, 2023 at 20:24 | comment | added | chrysante | Implementing the conversion check proposed in your example based on whether you're in the if-block or not may be trivial in this example, but in general its practically unsolvable because it's equivalent to the halting problem | |
| May 22, 2023 at 20:17 | history | asked | CPlus | CC BY-SA 4.0 |