mirror of https://lore.kernel.org/lkml/
 help / color / mirror / Atom feed
From: Dan Carpenter <error27@gmail.com>
To: Andi Kleen <andi@firstfloor.org>
Cc: linux-kernel@vger.kernel.org
Subject: Re: smatch 1.53 released
Date: Thu, 4 Jun 2009 21:50:08 +0200	[thread overview]
Message-ID: <a63d67fe0906041250v6e4252c2g594322a3a49e7307@mail.gmail.com> (raw)
In-Reply-To: <87iqjedf2a.fsf@basil.nowhere.org>

On 6/2/09, Andi Kleen <andi@firstfloor.org> wrote:
> Dan Carpenter <error27@gmail.com> writes:
>
>> Smatch is a source code checker for C.  Right now the focus is on checking
>>
>> for kernel bugs.
>
> Could you give a quick overview on what kinds of bugs it looks for
> and where the limitations are?
>

It's pretty good at finding locking bugs.  It also checks for double
kfree() bugs, null pointer dereferences and also if you check for null
instead of checking for PTR_ERR().  There is a check for using kfree()
instead of kfree_skb() as well.

The cool thing about smatch is that it's pretty easy to write custom
checks.  It's uses sparse as a C parser so you have to look through
expression.h to figure out how to do the pattern matching.  There is a
small example script which shows how that works.
http://repo.or.cz/w/smatch.git?a=blob;f=check_template.c

So you use sparse to grep the code for locking functions and then you
use set_state() to set the state to "locked".

If your code looks like this:
lock_kernel();
if (foo) {
        unlock_kernel();
} else {
        frob();
}
<--  Here the state can be either "locked" or "unlocked".
Calling get_state() here will tell you that it is state &merged.  You
can use get_possible() to get a list of possible states it could be.

Say later code looked like this:
if (!foo) {
<--  Here the state is "locked" because of the !foo.  Smatch figures
this out automatically, that comes from the "implications" module.  Do
other code checkers do this?  I'm pretty proud of the feature either
way.  :)
}

So basically you grep for locking functions and you set the state
based on that, then you grep for return statements and check that the
state is correct or print an error.  Smatch tracks the code paths in
the background and merges states or sets implied states.

Limitations:  The big limitation is that smatch only does one pass
through the code so loops aren't handled correctly.  Eventually it
will do two passes.

A lot of null dereference false positives come from places where it's
hard to tell if a loop is true at least once.
x = NULL;
while (param--) {
        x = &something;
}
x->member;
Someone reading the code probably knows what param is and that it's
non-zero at the start.  There is a "--assume-loops" option to make
smatch assume loops go through once.

Many of the locking false positives come from places where the unlock
happens in a seperate function.  It should be relatively straight
forward to make a list functions to say that if frob_the_module()
returns -12, or -14 that implies it unlocked a certain lock.  I
haven't done this yet.

Otherwise, it's still very young code.  Ideally smatch would know the
possible values of every variable in a function but right now many
variables just default to &undefined.  The implication code is not as
good as it could be.  Also I don't have a good way to build call trees
yet.  There is a lot of work to do at every level.

Still, it doesn't hurt to run smatch on your code before submitting a
patch.  There is an easy script for this:  kchecker /path/to/code.c.
Some of my accepted kernel patches have had bugs which could have been
caught by the current version of smatch...

regards,
dan carpenter

> Thanks,
>
> -Andi
>
> --
> ak@linux.intel.com -- Speaking for myself only.
>

  reply	other threads:[~2009-06-04 19:58 UTC|newest]

Thread overview: 7+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2009-06-02  8:41 Dan Carpenter
2009-06-02 11:56 ` Andi Kleen
2009-06-04 19:50   ` Dan Carpenter [this message]
2009-06-04 20:10     ` Andi Kleen
2009-06-05 13:52       ` Dan Carpenter
2009-06-09  6:15     ` Christian Kujau
2009-06-16 14:54       ` Dan Carpenter

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=a63d67fe0906041250v6e4252c2g594322a3a49e7307@mail.gmail.com \
    --to=error27@gmail.com \
    --cc=andi@firstfloor.org \
    --cc=linux-kernel@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 a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox

all inboxes | Powered by JetHome®