Hacker News Reader

Comment by drfuchs | Hacker News Reader

It sounds like you’re claiming that Coverity has a solution to the Halting Problem? That would indeed be magical.

Uh, no? Null pointers are far from the halting problem, though.

And to be clear, there are still limitations. It can't say if any value you pass into a function that is not part of the current compilation is safe. For somewhat obvious reasons.

But for a large large class of bugs, using advanced tooling can go a long way. As evidenced by the power of the advanced tooling new languages bring into the compilers. :)

The claim seems to be that the tool will always tell you absolutely whether a null-dereference will happen, and never say “maybe.” The Halting Problem is trivially reducible to this (just put an intentional null-deref in front of each halt).

Not necessarily the same point being made. At least, they are subtly different, to my understanding.

It can tell you that, "if this line is reached, and it was called from this path (with evidence on how this could happen), it will dereference a null." It is not saying that "running this program will guarantee give you a null dereference."

The halting problem is more in line with "this program will terminate on any possible inputs", which is more expansive. It is trivial to say that you can prove some programs won't terminate on a particular input. Question is if you can do it for all inputs, no?

Rice's theorem is a bit more direct here: C is Turing complete, some C programs derefernce null pointers, and some don't. Therefore, the question of whether a an arbitrary C program derefernces a null pointer is in general undecidable.

But I don't think the Op was claiming it was possible to do this perfectly, just possible to write very useful tools. You will always have either flase positives or false negatives (or I suppose inputs where you just hang).

Turing completeness is the bane of static analysis, but that doesn't make it a fruitless endeavor.

I wouldn't say that Rice's thm is the bane of static analysis. It is what makes the field interesting. If the problems were not undecidable then we wouldn't have do so many interesting and challenging things to make working tools.

Reminds me c compilers will bitch if a variable is unused. That's basically the same problem. And sometimes the compiler will flag something that won't happen because the code path is a phantom[1].

[1] Recent headline 'Phantom Code Paths Found Harmful'

I think you may be conflating the Halting Problem. The problem simply states whether it can be determined that a program, given a set of inputs, will eventually halt. Attempting to use a null pointer can be deterministic at compile time but it's not telling you that your program would halt or not.

A tool that can reliably tell whether a given program will hit a null deference or not can also trivially be repurposed to solve the Halting Problem. Thus, no such perfect deref tool can exist. The best you can claim is that there’s a tool with few false positives and false negatives. But the original post seems to claim that there’s a perfect one.

Sure, for an arbitrary program that is. One that is annotated to specify if a function returns/accepts null is a subset of this that is solveable.

The halting problem is used as a means to stick one's head in the sand. The halting problem imo is fundamentally uninteresting. A question that's almost as useful and is answerable is whether a program might not halt. Using your mapping to nullability, this tries to answer whether a pointer might be null. That's all the tools are trying to do and the halting problem doesn't get in the way.

No, it can't. You are just playing around with a problem you don't understand (null checks have 0 to do with the halting problem, it's always possible to know that a value will never be null in Java at compile time as long as you have all the source code - no dynamic libraries loaded at runtime)... unless you can actually show the proof of that, that would be really interesting to see.

It doesn't sound like the OP is claiming that at all, Coverity and tools like it use a technique called Symbolic Execution [0]

[0]. https://en.wikipedia.org/wiki/Symbolic_execution

While the halting problem can be pretty important in some cases, it's not very relevant in most day to day code. If you're not sure if your code will ever terminate, that usually means that you're doing something wrong.

So sure, sometimes Coverity will fail because of the halting problem, and in those cases it can give an appropriate error message. Most of the time, though, it'll work just fine and be a very useful tool.

Only the experimental Coverity Hypercomputing branch ;-)

Reply on news.ycombinator.com