Re: Super Lint (was: Unexecutable Stack / Buffer Overflow

[Randall R Schulz]

Horst,

One thing about what you say confuses me a bit. If a "complete and 
sound formal semantic[s] for C" is so difficult, what are compiler 
writers using when they write code generators for C (or any other 
procedural programming language)? It seems that if there is something 
missing or unintentionally ambiguous in the existing specifications 
(regardless of how formal you consider them) of the language, then it 
would not be possible to write reliable or predictable programs at 
all.

I'm not sure that the well-known theoretical insolubility of the 
halting problem implies that one cannot formally and tractably 
compute other meaningful and useful execution properties of an 
arbitrary procedural program. Is there other theoretical work along 
the lines of the halting problem that bear on this endeavor?

What do you suppose is the "bottom line" of practicality and 
feasibility of this or any attempt to infer execution properties of 
everyday programs? In your opinion, is it a blind alley, or a 
worthwhile avenue of investigation?

In thinking about this issue, one other thing that occurred to me is 
that abandoning the kinds of ad-hoc protocol specifications we now 
use in favor of a CORBA-like interface definition language might 
obviate these concerns. Of course, even if that approach were to 
prove fruitful, it would still be a long time before all the 
important protocols now in use could be replaced with those based on 
higher-level specifications of the interfaces and reliable (proven?) 
sub-programs for encoding and decoding (a.k.a. marshaling and 
unmarshaling) of operation parameters and returns.

Randy Schulz
Mountain View, CA USA

At 01:35 +0200 1/3/00, Horst von Brand wrote:
>....
>
>For full generality you need a complete and sound formal semantic for
>C. And that is _extremely_ hard, if indeed possible. In the end, you will
>hit the halting problem, so you will _always_ underestimate the "can't
>happen", and that is exactly what irritates me the most of such tools.
>
>BTW, much of what you are describing is exactly what the compiler has to do
>to discover optimization oportunities.  I assume that is why lints fell
>into disfavour, partly because of ANSI C prototypes (the original lint
>served mostly to detect mismatches between declarations and uses) and stuff
>like gcc's -Wall can be had almost for free in the compiler.
>--
>Horst von Brand                             [e-mail]