Limitations and Evolution [LWN.net]

Limitations and Evolution

Posted Apr 3, 2006 17:15 UTC (Mon) by AnswerGuy (guest, #1256)
In reply to: Coverity: one bug fixed every six minutes by anLWNreader
Parent article: Coverity: one bug fixed every six minutes

Clearly there are limits to the types of bugs that can be found through static analysis of C programs. (If nothing else the halting problem and Godel's Theorem are clear indications that no form of analysis can guarantee that any non-trivial code in any "sufficiently powerful" language (or other axiomatic system) is bug free.

However, we can do far better than our current limits if we also adopt some programming extensions and programming practices that make the job easier. For example C would benefit from much more extensive use of assertions ... and some language features to support static and stochastic simulation tests which incorporate those assertions --- and some features for PBC (programming by contract) --- (ultimately three specific forms of assertions: pre-conditions, invariants and post conditions).

I recall that Coverity evolved out of the Stanford Checker, which used a modified version of gcc (called xgcc). Of course Engler and his team never distributed any derivative of their work. Ergo they have never been obliged to release their sources. However, I think it's high time a group in the open source community undertook a similar approach.

There are limits to what can be accomplished by static code analysis. But the yields are low hanging fruit which should be plucked as efficiently as possible so we can leave our best and brightest minds free to focus on more interesting problems.

JimD

Limitations and Evolution

Posted Apr 3, 2006 17:36 UTC (Mon) by madscientist (subscriber, #16861) [Link]

I realize you never claimed otherwise, directly, but to be clear Coverity no longer uses GCC, modified or not. They are now using a different code parsing front-end, which is proprietary.

Limitations and Evolution

Posted Apr 3, 2006 21:43 UTC (Mon) by iabervon (subscriber, #722) [Link] (4 responses)

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.

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.

Limitations and Evolution

Posted Apr 3, 2006 23:30 UTC (Mon) by cventers (guest, #31465) [Link] (2 responses)

Well... I'm not a big fan of excessive assertions or runtime PBC. There is
a point where it's very obnoxious, because you're wasting time for every
single operation just to make sure you (the programmer) didn't make a
certain mistake.

I'm not totally against error checking; indeed, I think you should
vigorously meter anything coming in and out of your program or library. My
own code is extremely anal about checking the return value of every system
call / library call. It's almost always possible for my program to back
out from and continue operating when it encounters, say, a malloc()
failure, etc.

I've found in my own experience that if you build your code very anally in
this way, you end up with something that is *very* fault tolerant, and if
and when it does fail, it fails very close to the bug site (rather than
halfway across the app).

Limitations and Evolution

Posted Apr 4, 2006 0:20 UTC (Tue) by dlang (guest, #313) [Link] (1 responses)

this isn't a runtime tool

Limitations and Evolution

Posted Apr 4, 2006 0:44 UTC (Tue) by jtc (guest, #6246) [Link]

"this isn't a runtime tool"

That's right! To elaborate: DBC is not a run-time tool, although some toolsets that support DBC provide useful runtime-checking facilities (checking assertions, preconditions, etc. at run time). The main point of DBC is to document precise specifications for interfaces, which allow clients (programmers using the specifications) to use the interfaces correctly and to make it easier to discover defects in software that uses these interfaces (whether by testing or inspection).

Run-time checking of assertions certainly is useful, but often must be turned off in production systems for efficiency.

Limitations and Evolution

Posted Apr 4, 2006 0:34 UTC (Tue) by jtc (guest, #6246) [Link]

"However, we can do far better than our current limits if we also adopt some programming extensions and programming practices that make the job easier. For example C would benefit from much more extensive use of assertions ... and some language features to support static and stochastic simulation tests which incorporate those assertions --- and some features for PBC (programming by contract) --- (ultimately three specific forms of assertions: pre-conditions, invariants and post conditions)."

AKA design by contract (DBC):

http://en.wikipedia.org/wiki/Design_by_contract

Limitations and Evolution

Posted Apr 4, 2006 9:06 UTC (Tue) by eru (subscriber, #2753) [Link] (4 responses)

For example C would benefit from much more extensive use of assertions ... and some language features to support static and stochastic simulation tests which incorporate those assertions --- and some features for PBC (programming by contract) --- (ultimately three specific forms of assertions: pre-conditions, invariants and post conditions).

IMHO C would benefit most from some minor language changes that would remove the most commonly recurring idiotic mistakes at the time the code is first compiled! At the top of my list would be:

Introduce a proper Boolean type distinct from integers, make comparisons return it, and all conditional control structures require it. This gets rid of most "=" vs "==" errors. The rest would go away by making it an error if the return value of operator "==" is unused.
Enforce separation of pointers from integers better. Don't allow bare 0 as a NULL pointer constant.
Disallow calling extern functions without the presence of a prototype.
Introduce separate keywords for breaking loops and breaking from switch branches. (There actually was a widespread phone servide outage in the USA about a decade ago that would not have happened if C had had this feature...)
Require fall-through in switches to be explicitly indicated by a new keyword (this would naturally apply only to non-empty branches, so "case 1: case 2: case 3: ..." would be unaffected).
Make it an error if there is a code path through which a non-void function might return without specifying a return value.

These changes would greatly reduce C bugs without affecting efficiency at all, or make programs any more verbose. Of course existing programs would need modifications, but these could be largely automated.

Limitations and Evolution

Posted Apr 4, 2006 15:11 UTC (Tue) by vmole (guest, #111) [Link] (3 responses)

Umm, "minor changes"? I don't think breaking 99.9%[1] of the existing code base is "minor".

Which isn't to say they aren't good ideas for a language, but you'll never get them added to C, except possibly the required prototype one (which a lot of compilers can enforce now) and the wrong or missing return type (ditto).

[1] Totally made up statistic. Don't whine.

Limitations and Evolution

Posted Apr 5, 2006 5:41 UTC (Wed) by eru (subscriber, #2753) [Link] (2 responses)

Umm, "minor changes"? I don't think breaking 99.9%[1] of the existing code base is "minor".

As I already aknowledged in my last sentence, existing programs would have to be changed (even though most changes could be automated). In that sense the changes are not "minor". But on the other hand the resulting language would still be almost identical to C, it would retain all the good features of C, and programmers would quickly get used to the modified rules.

Getting this into the official C standard is of course hopeless. but it would probably not be too much work to implement it as an option in GCC.

Automatically make buggy code pass static checkers! Yay!

Posted Apr 6, 2006 0:59 UTC (Thu) by xoddam (subscriber, #2322) [Link] (1 responses)

> most changes could be automated

You mean, you could automatically convert existing buggy
code into something semantically identical which passes
all your new-fangled static checking.

>... it would probably not be too much work to implement it
> as an option in GCC.

splint already supports most of the things you suggest, without
changes to the syntax of C itself (it uses comments and/or
macros) or to the semantics of existing code. Running an
extra checker over the source isn't very much different from
enabling a compiler option. And like -Wall and -Werror, you
can gradually fix warnings by hand, then decide on a per-compilation-unit
basis when to enforce them.

http://www.splint.org

Missing my point...

Posted Apr 6, 2006 5:51 UTC (Thu) by eru (subscriber, #2753) [Link]

> most changes could be automated

You mean, you could automatically convert existing buggy code into something semantically identical which passes all your new-fangled static checking.

You miss my point. I was just addressing backward-compatibility concerns when initally moving a lot of code to the new system. Certainly a conversion of a buggy program is still a buggy program (although the converter should highlight dubious bits in the code for possible corrections). The real value of the proposed new rules would be realized when writing new code or hand-modifying old.

splint already supports most of the things you suggest, without changes to the syntax of C itself (it uses comments and/or macros) or to the semantics of existing code.

So why isn't it used more? Answer: precisely because it is an extra pass, it is not installed everywhere the compiler is, and it requires extra annotations to be really useful. Correctness is not an add-on feature. Programmers should mind it all the time when writing code, without imagining it can be retrofitted with a final lint run, or with testing. Having every compiler run nag about dubious code helps better in achieving this. Anyway, my proposed changes are really not so much about adding extra statical checking, but removing totally unnecessary error sources from the language.