From: wagi@monom.org (Daniel Wagner)
To: cocci@systeme.lip6.fr
Subject: [Cocci] Filter out field names
Date: Thu, 21 Jan 2016 10:47:54 +0100 [thread overview]
Message-ID: <56A0A94A.9070702@monom.org> (raw)
Hi,
I am trying to transform Linux kernel code in order to test for data
races. Let me illustrate this by an example
struct lpctx {
spinlock_t lock;
int cnt;
};
static struct lpctx *lpctx;
static void lpctx_good1(struct lpctx *lx)
{
spin_lock(&lx->lock);
lx->cnt++;
spin_unlock(&lx->lock);
}
static void lpctx_warning1(struct lpctx *lx)
{
lx->cnt++;
}
As you can see lptctx_warning1() is increasing the counter without
holding the lock. The main idea(*) is to annotate all accesses to lx by
adding a WARN_ON(!lock_is_held(&lx->lock.dep_map)).
Thanks to Julia's excellent help on IRC I have currently this somewhat
working cocci script:
@depends on patch@
struct lpctx *x;
identifier f;
statement S;
@@
( S
+ WARN_ON(!lock_is_held(&x->lock.dep_map));
&
x->f
)
This results in:
@@ -16,10 +16,13 @@ static void lpctx_good1(struct lpctx *lx
DBG("");
spin_lock(&lx->lock);
+ WARN_ON(!lock_is_held(&lx->lock.dep_map));
lx->cnt++;
+ WARN_ON(!lock_is_held(&lx->lock.dep_map));
spin_unlock(&lx->lock);
+ WARN_ON(!lock_is_held(&lx->lock.dep_map));
}
static void lpctx_warning1(struct lpctx *lx)
@@ -27,6 +30,7 @@ static void lpctx_warning1(struct lpctx
DBG("");
lx->cnt++;
+ WARN_ON(!lock_is_held(&lx->lock.dep_map));
}
There are a bunch of problems, e,g. the hard coded type/names or the
WARN_ON() should be put in front of the deferences but that is something
for later to improve. The main problem I face at this point is to filter
out the spin_lock() and spin_unlock() access. All my attempts didn't let
to the expected result. I think the best thing would be to match on the
type. So if 'f' is of type spinlock_t ignore it. Any ideas how this
could be expressed?
Thanks,
Daniel
(*) Talking with Nicholas over a coffee helps a lot. Thanks a lot!
next reply other threads:[~2016-01-21 9:47 UTC|newest]
Thread overview: 6+ messages / expand[flat|nested] mbox.gz Atom feed top
2016-01-21 9:47 Daniel Wagner [this message]
2016-01-21 11:02 ` [Cocci] Filter out field names Julia Lawall
2016-01-22 14:32 ` Daniel Wagner
2016-01-22 16:09 ` SF Markus Elfring
2016-02-26 10:40 ` Daniel Wagner
2016-02-26 12:40 ` SF Markus Elfring
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=56A0A94A.9070702@monom.org \
--to=wagi@monom.org \
--cc=cocci@systeme.lip6.fr \
/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.