Limitations and Evolution [LWN.net]

Limitations and Evolution

Posted Apr 3, 2006 21:43 UTC (Mon) by iabervon (subscriber, #722)
In reply to: Limitations and Evolution by AnswerGuy
Parent article: Coverity: one bug fixed every six minutes

The halting problem doesn't really matter for debugging; the halting problem means that you can't determine whether a flaw actually could cause problems in practice, but anything that you can't statically analyze in finite time is at least bad form, because other programmers won't be able to tell whether it works. Of course, the system has to be more clever than current systems are in order to make the same determinations that programmers do.

The real issue is that checking is only useful with a precise definition of what would be wrong. If it carefully does something which isn't actually what it's supposed to do, the static checker can't tell that that wasn't what it was supposed to do. For example, I've just had bugs where it was printing the wrong values for labels on a chart, and using the wrong string length for deciding how many labels to have. It would be impractical to write a checker which could identify that my generated chart shows things wrong.

to post comments

Limitations and Evolution

Posted Apr 3, 2006 23:53 UTC (Mon) by nix (subscriber, #2304) [Link] (3 responses)

Rice's theorem really *is* a problem, and that's a direct consequence of the halting problem. It pretty much condemns us to either using heuristics or always providing a way to bail out of an optimization that isn't getting anywhere.

Limitations and Evolution

Posted Apr 4, 2006 1:02 UTC (Tue) by iabervon (subscriber, #722) [Link] (2 responses)

Rice's theorem is only a problem if you consider a program okay if it never commits an array bounds violation (for example), even if it's impractical to demonstrate that it won't. But if it takes substantial analysis to determine that the program doesn't have a problem, than that's a bug anyway; at the very least, the next person to touch the code is likely to make a change that makes it misbehave.

Rice's theorem is a problem for compiler optimization, where you don't care whether the code is at all sane; you want to generate code that works regardless. And it's an issue for deciding whether to accept code to run, where you want to run any requested code which doesn't break any rules.

But a static checker doesn't have to worry too much about Rice's theorem (or decidability in general), because you want the code to not just be correct, but obviously correct. And that's a bit vague, but a finite limit on the complexity of the analysis that should be attempted to prove correctness is certainly appropriate.

Limitations and Evolution

Posted Apr 4, 2006 19:30 UTC (Tue) by nix (subscriber, #2304) [Link] (1 responses)

Unfortunately you don't need particularly contrived code to collide with Rice's theorem, in my experience :( even static checkers will frequently need to say `oh, I give up' and not warn about it, at least for some classes of test.

I wish this wasn't true. I want a better universe: this one's broken.

Limitations and Evolution

Posted Apr 4, 2006 20:15 UTC (Tue) by iabervon (subscriber, #722) [Link]

I think that's not so much a consequence of Rice's theorem as an effect of not supporting quite all of the sorts of constraints programmers use. A bigger issue is that, even for decidable questions of interest (e.g., is there a proof of the correctness of this code which would fit on a single page?) they're often NP-complete. So you get code with a comment explaining why it's okay, and programmers can check that it's true in polynomial time, but the static checker can't come up with the correct rule in a reasonable time (and, of course, the original programmer came up with the constraint first and then wrote the code to obey it). But that's an issue of feasibility, not decidability. This can be made practical with annotations and assertions, although these have to be made acceptable to programmers by being sufficiently readable and writable (so the programmer can write them without much trouble, and so other programmers find them helpful in understanding why the code works).

And, of course, a static checker is only really useful when the number of cases it fails to complete which people can tell are okay is low enough that it can usefully flag as flaws everything that it can't prove.