[ANNOUNCE] sparse-0.2-cl2 is now available

[ANNOUNCE] sparse-0.2-cl2 is now available

[Christopher Li]

Temporarily at:
    http://userweb.kernel.org/~chrisl/sparse-0.2-cl2

Will appear later at:
    http://ftp.kernel.org//pub/linux/kernel/people/chrisl/patches/sparse/sparse-0.2-cl2/


I have been play with sparse to add more Stanford checker style
of checking. The paper is "Checking System Rules Using System-
Specific, Programmer-Written Compiler Extensions" by Dawson Engler
etc.

Unlike the Stanford checker and smatch, this checker is working on
the linearization level instead of AST level. Linearization code
can be very convenient (when it works) to trace the data flow because
pseudo is in SSA form. There is define/user chain to avoid scan
every instruction.

I take the malloc checking for example to explain how the checker
works. The checking usually happen in three step:

The first step is scanning the linearize instruction. It look for
relevant operations. For malloc checker, the task is find out
the malloc/free function call and usage of malloced pointer.

The second step is converting the relevant operations into checker
instruction. The checker instruction is a simplification of the whole
program, only contain the operation relevant to checker.

The third step is executing the checker instruction. It try to execute
every possible execution flow in the function. The execution engine
will let the checker instruction perform state changes.

Thanks to step two, the size and complexity of the of program has been
greatly reduced.

The new checking has been very fast, it add a few seconds to the make C=1
run.

Again, comment and feed back are always welcome.

Chris

Change log in sparse-0.2-cl2:
 - adding pointer signedness fix
 - adding spinlock checking

Change log in sparse-0.2-cl1:
  The most interesting part is the inline function annotation.
  The new checker can find out inlined function usage. The interrupt
  checker does not depend on x86 asm instruction any more.


origin.patch
    006eff06c7adcfb0d06c6fadf6e9b64f0488b2bf URL: git://git.kernel.org/pub/scm/linux/kernel/git/josh/sparse.git
incompatible-ptr-signess
    Bug fix in pointer modifiers inherent at function degeneration.
sizeof-incomplete
    Fix double semicolon in struct declare
anon-symbol
    Fix core dump on anonymous symbol.
instruction-buffer-size
    Fix core dump on huge switch
debug-checker
    Adding debug option for showing the linearized instruction.
no-dead-instruction
    Disable liveness "dead" instruction by default.
ptr-allocator
    Make the ptrlist using the sparse allocator.
annotate-inline-2
    Add annotation for inline function call.
malloc-checker
    Adding the malloc NULL pointer checker.
interrupt-checker
    Adding the interrupt checker
spinlock-checker
    Adding spinlock checker


Total 12 patches

Re: [ANNOUNCE] sparse-0.2-cl2 is now available

[Andi Kleen]

Christopher Li <sparse@chrisli.org> writes:
> 
> Change log in sparse-0.2-cl2:
>  - adding pointer signedness fix
>  - adding spinlock checking


Interesting. Did you find any kernel bugs with this?

-Andi

Re: [ANNOUNCE] sparse-0.2-cl2 is now available

[Christopher Li]

On Sat, Feb 10, 2007 at 06:33:25PM +0100, Andi Kleen wrote:
> Interesting. Did you find any kernel bugs with this?

In short, not very useful yet.

The current run of of sparse-0.2-cl2 on git default i386 config
will find about 6 place kernel using allocated memory without NULL
check. But Linus said most of them is not worthy checking because
it is in the early stage of the kernel initializations.
It just can't fail on those small memory allocation. May be one
of them worth adding the NULL check.

For interrupt and spinlock checking, it less noisier than the current
sparse context level checking. The new checker code can identify inline
function call, so it has more information. But it is still too noisy.
I did not look at every interrupt and spinlock warning. From what I saw,
it show limit of the checker itself rather than a bug in kernel.

A lot of false positive is come from we don't have enough information
inside a single function.

e.g. sparse has not way to know some function only get called with interrupt
disabled (or some lock already hold). So it assume interrupt is still
enable and generate wrong warnings. Another example is that some helper
function will wrap the locking function. Complain about the exit with locking
hold is wrong.

I am hoping adding the cross function checking will reduce those false positive.
Any way, it need more information to reduce false positive.

I am still working on the cross function checking. May be it will become
more useful one day.

Chris

Re: [ANNOUNCE] sparse-0.2-cl2 is now available

[Al Viro]

On Sat, Feb 10, 2007 at 09:17:58PM -0800, Christopher Li wrote:
> e.g. sparse has not way to know some function only get called with interrupt
> disabled (or some lock already hold). So it assume interrupt is still
> enable and generate wrong warnings. Another example is that some helper
> function will wrap the locking function. Complain about the exit with locking
> hold is wrong.
> 
> I am hoping adding the cross function checking will reduce those false positive.
> Any way, it need more information to reduce false positive.
> 
> I am still working on the cross function checking. May be it will become
> more useful one day.

I have some stuff in that direction, but it take some resurrecting...

Re: [ANNOUNCE] sparse-0.2-cl2 is now available

[Christopher Li]

On Sun, Feb 11, 2007 at 05:50:15AM +0000, Al Viro wrote:
> 
> I have some stuff in that direction, but it take some resurrecting...

OK, we should talk.

Here is what I have:

Linearize bytecode writer, which produce the binary linearized code.
The uncompress size is about 10 times the i386 .o file. I don't have
the loader ready to verify it yet. It is aim at fast loading bytecode
and simple, I havn't done much toward optimized the code size.

If we keep it 10 times over head, my home computer can load the full linux
kernel and have some spare for checking.

I am still working on the bytecode loader and linker for merging symbols.
It need to answer the question:

Which file define which function.
Which external symbol does this function use.

Once we get the function user/define chain, it can enable a lot of new checking.

The current linearized code is not very friendly to linking because we
keep abstract declare and real declare as different node. Depend on the
position, the caller will get different node even in one file.
 
I am going to take out the LKML on later email because discussion is
more sparse specific now.

Chris

Re: [ANNOUNCE] sparse-0.2-cl2 is now available

[Andi Kleen]

> 
> If we keep it 10 times over head, my home computer can load the full linux
> kernel and have some spare for checking.
> 
> I am still working on the bytecode loader and linker for merging symbols.
> It need to answer the question:
> 
> Which file define which function.
> Which external symbol does this function use.
> 
> Once we get the function user/define chain, it can enable a lot of new checking.

At least for interrupts on/off you'll likely need new annotations because
this state can be changed in assembly files before/after calling out to 
C.

For locks this fortunately cannot happen (at least not on x86*) 

-Andi