lkml.org 
[lkml]   [2000]   [Jan]   [6]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: Super Lint
vonbrand@sleipnir.valparaiso.cl (Horst von Brand)  wrote on 02.01.00 in <200001021555.MAA01783@sleipnir.valparaiso.cl>:

> Jeff Dike <jdike@karaya.com> said:
> > [ Resend - accidentally sent it as a private reply instead of to the
> > > list...] Is this 'super-lint' something that could/should be implemented
> > > in something like 'cxref' and included in documentation?
>
> > This super-lint is not something that you're going to toss into cxref.
> > It's a hard problem.
>
> One start in that direction (that I don't particularly like, BTW, as it
> needs much assistance from the programmer, and seems to make certain legal
> constructions like handling linked lists totally impossible) is lclint,
> from somewhere on MIT AFAIR.

If it makes linked lists impossible, it's going about things the wrong
way.

> 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

The really hard part is the stuff about sequence points and how they make
for undefined behaviour. I gather the C0X draft currently has an appendix
that has a somewhat formal for exactly this.

> 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.

I'm not quite sure if you think it's going to find too many or too few
bugs.

Anyway, as anyone who's done mathematical proofs knows, you don't really
need the fully general thing anyway. That's what you have a programmer
for. You tell the thing what is supposed to happen, and the thing verifies
that this is indeed what happens, or otherwise tells you that it can't
figure this out and you'll have to look for yourself.

Currently, you have to control _everything_. With such a tool, you should
be able to reduce this to very few parts of a program.

It's far easier to check a few small routines than to check all of a big
program. Just as it's easier to verify that a call to snprintf gives the
right buffer size, and that snprintf does the right thing with a buffer
size, than that a call to sprintf will never overflow a buffer.

In fact, good advice for writing security-critical code is to design
interfaces to avoid these problems in the first place.

If you absolutely must have variable-sized buffers, always have a buffer
length in the parameter list. Better would be to only handle a buffer
descriptor around that points to a buffer the called routine can adjust
the size of as needed - has the added benefit of avoiding hardcoded
maximum sizes.

> 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.

Also because, while there was a free gcc, there wasn't a free lint for
quite a long time.

MfG Kai

-
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@vger.rutgers.edu
Please read the FAQ at http://www.tux.org/lkml/

\
 
 \ /
  Last update: 2005-03-22 13:55    [W:0.046 / U:0.060 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site