All of lore.kernel.org
 help / color / mirror / Atom feed
From: Christopher Li <sparse@chrisli.org>
To: linux-sparse@vger.kernel.org
Cc: linux kernel mail list <linux-kernel@vger.kernel.org>,
	Josh Triplett <josh@freedesktop.org>
Subject: [ANNOUNCE] sparse-0.2-cl2 is now available
Date: Fri, 9 Feb 2007 16:00:55 -0800	[thread overview]
Message-ID: <20070210000055.GA19968@chrisli.org> (raw)
In-Reply-To: <20070204085329.GA6520@chrisli.org>


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



  reply	other threads:[~2007-02-10  0:43 UTC|newest]

Thread overview: 7+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2007-02-04  8:53 [ANNOUNCE] sparse-0.2-cl1 is now available Christopher Li
2007-02-10  0:00 ` Christopher Li [this message]
2007-02-10 17:33   ` [ANNOUNCE] sparse-0.2-cl2 " Andi Kleen
2007-02-11  5:17     ` Christopher Li
2007-02-11  5:50       ` Al Viro
2007-02-11  6:02         ` Christopher Li
2007-02-11 10:41           ` Andi Kleen

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=20070210000055.GA19968@chrisli.org \
    --to=sparse@chrisli.org \
    --cc=josh@freedesktop.org \
    --cc=linux-kernel@vger.kernel.org \
    --cc=linux-sparse@vger.kernel.org \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.