From: Julia Lawall <julia.lawall@inria.fr>
To: Markus Elfring <Markus.Elfring@web.de>
Cc: Yuan Can <yuancan@huawei.com>, cocci@inria.fr
Subject: [cocci] usage of locks
Date: Sun, 25 Sep 2022 19:12:12 +0200 (CEST) [thread overview]
Message-ID: <alpine.DEB.2.22.394.2209251906090.3293@hadrien> (raw)
Here is an alternative semantic patch to the one proposed by Yuan Can. It
checks across the entire kernel for lock declarations, initializations and
locks, and reports on locks that are declared but seem not to be
initialized, not to be locked, or both. There may be false positives due
to problems in parsing the functions that initialize or lock the locks.
Another reason for false positives is the use of typedefs that make the
type at the point of declaraion and at the point of initialization or
locking appear to be different.
When a lock has a distinctive name, it is easy to check the results using
grep. Unfortunately, many locks are called "lock".
Yuan Can (or anyone else), if you find some bugs that are worth fixing,
please go ahead.
julia
#spatch --include-headers --recursive-includes --include-headers-for-types
@initialize:ocaml@
@@
let created = Hashtbl.create 101
let created_array = Hashtbl.create 101
let initialized = Hashtbl.create 101
let locked = Hashtbl.create 101
let possible_init = Hashtbl.create 101
let possible_lock = Hashtbl.create 101
let other = Hashtbl.create 101
@create1@
identifier t,f;
position pl;
typedef spinlock_t;
@@
struct t {
...
spinlock_t f@pl;
...
}
@script:ocaml@
t << create1.t;
f << create1.f;
p << create1.pl;
@@
Hashtbl.replace created ("struct "^t,f) p
@create2@
identifier t,f;
position pl;
typedef spinlock_t;
@@
struct t {
...
struct mutex f@pl;
...
}
@script:ocaml@
t << create2.t;
f << create2.f;
p << create2.pl;
@@
Hashtbl.replace created ("struct "^t,f) p
@create3@
identifier t,f;
position pa;
typedef spinlock_t;
@@
struct t {
...
spinlock_t f@pa[...];
...
}
@script:ocaml@
t << create3.t;
f << create3.f;
p << create3.pa;
@@
Hashtbl.replace created_array ("struct "^t,f) p
@create4@
identifier t,f;
position pa;
typedef spinlock_t;
@@
struct t {
...
struct mutex f@pa[...];
...
}
@script:ocaml@
t << create4.t;
f << create4.f;
p << create4.pa;
@@
Hashtbl.replace created_array ("struct "^t,f) p
(* ------------------------------------------------- *)
(* check for standard initializations and locks *)
@init@
type t;
t o;
identifier f;
position p;
@@
\(spin_lock_init\|mutex_init\|__mutex_init\|__mutex_rt_init\)(\(&o.f@p\|&o.f@p[...]\))
@script:ocaml@
t << init.t;
f << init.f;
p << init.p;
@@
Hashtbl.replace initialized (t,f) p
@init1@
identifier t,i,f;
position p;
@@
struct t i = {
.f@p = __SPIN_LOCK_UNLOCKED(f),
};
@script:ocaml@
t << init1.t;
f << init1.f;
p << init1.p;
@@
Hashtbl.replace initialized ("struct "^t,f) p
@lock@
type t;
t o;
identifier f;
identifier lock = {spin_lock,spin_lock_bh,spin_lock_irqsave,spin_lock_irq,spin_lock_nested,
spin_trylock,spin_trylock_bh,spin_trylock_irqsave,spin_trylock_irq,
mutex_lock,mutex_trylock,mutex_lock_nested,mutex_lock_interruptible,mutex_lock_killable,mutex_lock_io};
position p;
@@
lock(\(&o.f@p\|&o.f@p[...]\),...)
@script:ocaml@
t << lock.t;
f << lock.f;
p << lock.p;
@@
Hashtbl.replace locked (t,f) p
(* ------------------------------------------------- *)
(* check for aliases or non-standard uses *)
@alias1@
type t;
t o;
identifier f;
position p;
expression x;
{spinlock_t,struct mutex} *e;
@@
(
x = e
&
x = \(&o.f@p\|&o.f@p[...]\)
)
@script:ocaml@
t << alias1.t;
f << alias1.f;
p << alias1.p;
@@
Hashtbl.replace initialized (t,f) p;
Hashtbl.replace locked (t,f) p
@alias2@
type t;
t o;
identifier f;
position p;
{spinlock_t,struct mutex} *e;
@@
(
return e;
&
return \(&o.f@p\|&o.f@p[...]\);
)
@script:ocaml@
t << alias2.t;
f << alias2.f;
p << alias2.p;
@@
Hashtbl.replace initialized (t,f) p;
Hashtbl.replace locked (t,f) p
@alias3@
type t;
t o;
identifier f;
expression ifn =~ "init";
expression lfn =~ "lock";
expression ofn != mutex_destroy;
position p;
{spinlock_t,struct mutex} *e;
@@
\(ifn\|lfn\|ofn\)(...,
(
e
&
\(&o.f@p\|&o.f@p[...]\)
)
,...)
@script:ocaml@
t << alias3.t;
f << alias3.f;
p << alias3.p;
ifn << alias3.ifn;
@@
Hashtbl.replace possible_init (t,f) (p,ifn)
@script:ocaml@
t << alias3.t;
f << alias3.f;
p << alias3.p;
lfn << alias3.lfn;
@@
Hashtbl.replace possible_lock (t,f) (p,lfn)
@script:ocaml@
t << alias3.t;
f << alias3.f;
p << alias3.p;
ofn << alias3.ofn;
@@
Hashtbl.replace other (t,f) (p,ofn)
(* ------------------------------------------------- *)
@finalize:ocaml@
cs << merge.created;
ss << merge.created_array;
is << merge.initialized;
ls << merge.locked;
pi << merge.possible_init;
pl << merge.possible_lock;
ot << merge.other;
@@
let redo l tbl =
List.iter (Hashtbl.iter (Hashtbl.replace tbl)) l in
redo cs created;
redo ss created_array;
redo is initialized;
redo ls locked;
redo pi possible_init;
redo pl possible_lock;
redo ot other;
let clean s =
match Str.split (Str.regexp (!Flag.dir^"/")) s with
[x] -> x
| _ -> s in
let check_possible s k possible other =
try
let (p,fn) = Hashtbl.find possible k in
Printf.sprintf " (possible %s via call to %s in %s:%d)"
s fn (clean((List.hd p).file)) (List.hd p).line
with Not_found ->
try
let (p,fn) = Hashtbl.find other k in
Printf.sprintf " (possible %s via call to %s in %s:%d)"
s fn (clean((List.hd p).file)) (List.hd p).line
with Not_found -> "" in
let collect s created =
Hashtbl.fold
(fun ((t,f) as k) p r ->
let file = clean ((List.hd p).file) in
let line = (List.hd p).line in
let isinit = Hashtbl.mem initialized k in
let islocked = Hashtbl.mem locked k in
match (isinit,islocked) with
(true,true) -> r
| (true,false) ->
let p = Hashtbl.find initialized k in
(1,Printf.sprintf
"%slock %s.%s declared in %s on line %d is initialized in %s on line %d, but is never locked%s"
s t f file line (clean((List.hd p).file)) (List.hd p).line
(check_possible "lock" k possible_lock other)) :: r
| (false,true) ->
let p = Hashtbl.find locked k in
(2,Printf.sprintf "%slock %s.%s declared in %s on line %d is locked in %s on line %d, but is never initialized%s"
s t f file line (clean((List.hd p).file)) (List.hd p).line
(check_possible "init" k possible_init other)) :: r
| (false,false) ->
(3,Printf.sprintf "%slock %s.%s declared in %s on line %d is never locked or initialized%s%s"
s t f file line
(check_possible "init" k possible_init other)
(check_possible "lock" k possible_lock other)) :: r)
created [] in
let r1 = collect "" created in
let r2 = collect "array " created_array in
let res = List.sort compare (List.append r1 r2) in
List.iter (fun x -> Printf.printf "%s\n" (snd x)) res
next reply other threads:[~2022-09-25 17:12 UTC|newest]
Thread overview: 22+ messages / expand[flat|nested] mbox.gz Atom feed top
2022-09-25 17:12 Julia Lawall [this message]
2022-09-25 19:48 ` [cocci] Checking the usage of locks with SmPL Markus Elfring
2022-09-28 9:24 ` Markus Elfring
2022-09-26 7:36 ` Markus Elfring
2022-09-26 7:52 ` Julia Lawall
2022-09-26 8:23 ` Markus Elfring
2022-09-26 18:42 ` Markus Elfring
2022-09-28 19:05 ` Markus Elfring
2022-09-28 19:26 ` Julia Lawall
2022-09-28 19:34 ` Markus Elfring
2022-09-28 19:38 ` Julia Lawall
2022-09-29 6:21 ` Markus Elfring
2022-09-29 6:43 ` Julia Lawall
2022-09-29 7:40 ` Markus Elfring
2022-09-29 7:56 ` Julia Lawall
2022-09-29 9:07 ` Markus Elfring
2022-09-29 9:18 ` Julia Lawall
2022-09-29 9:40 ` Markus Elfring
2022-10-03 7:21 ` [cocci] Checking explanations for SmPL functionality Markus Elfring
2022-10-03 7:29 ` Julia Lawall
2022-10-03 7:36 ` Markus Elfring
2022-10-03 12:52 ` 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=alpine.DEB.2.22.394.2209251906090.3293@hadrien \
--to=julia.lawall@inria.fr \
--cc=Markus.Elfring@web.de \
--cc=cocci@inria.fr \
--cc=yuancan@huawei.com \
/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;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).