Re: Kernel code analysis (was Re: "movb" for spin-unlock (was Re: namei() query))

From: Horst von Brand (vonbrand@sleipnir.valparaiso.cl)
Date: Sat Apr 22 2000 - 13:59:41 EST


Jeff Garzik <jgarzik@mandrakesoft.com> said:
> Jamie Lokier wrote:

[...]

> The tool which I envision need only handle simple stuff at first. As
> long as the source code analyzer knows C code at a semantic level, I
> need only write extra rules / regexes to catch basic but very common
> driver code errors.

> It is too much to ask "kernel-lint" to puzzle through page cache flag
> arcana for example, but I can think of a ton of simple things that a
> kernel-lint tool could scan for that would be useful..

> * divide by power of two, instead of shifting

Bug your neighborly compiler writer to optimize that one

> * calling pci_find_xxx functions without pci_enable_device somewhere in
> the driver

grep(1)

> * calling MOD_INC_USE_COUNT in a function AFTER a call to request_irq or
> a similar function which may sleep

A bit of perl perhaps?

> It's still a tall order to handle simple stuff like this.. Further, it
> is granted that all rules are generally broken for a good reason at
> least once. but such a tool IMHO would be invaluable to people
> maintaining kernel drivers.

What is truly needed is to be able to check properties over all paths, like
that locks are taken (or not, as may be) and then released; that interrupts
are (or not) turned off, etc. Local stuff like the above is (somewhat) easy
to check with existing tools, perhaps adding a bit of cpp hackery to
#define stuff so it screams #error when it is used wrong or used when it
shouldn't be (just to be used as a #included sanity gcc run check, not in
production), etc.

-- 
Horst von Brand                             vonbrand@sleipnir.valparaiso.cl
Casilla 9G, Viņa del Mar, Chile                               +56 32 672616

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



This archive was generated by hypermail 2b29 : Sun Apr 23 2000 - 21:00:21 EST