Limitations and Evolution [LWN.net]

Limitations and Evolution

Posted Apr 4, 2006 1:02 UTC (Tue) by iabervon (subscriber, #722)
In reply to: Limitations and Evolution by nix
Parent article: Coverity: one bug fixed every six minutes

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.

to post comments

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.