[cocci] usage of locks

[cocci] usage of locks

[Julia Lawall]

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

Re: [cocci] Checking the usage of locks with SmPL

[Markus Elfring]

> Here is an alternative semantic patch to the one proposed by Yuan Can.


Thanks for another contribution.



> …                                        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.


Will such background information trigger further development considerations?


Would you like to achieve any improvements for safer scope (or name) resolution?


> @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[...]\))


How do you think about to apply the following SmPL coding style variant?

(spin_lock_init
|mutex_init
|__mutex_init
|__mutex_rt_init
)(&o.
(f@p
|f@p[...]
))


Can a reordering become helpful for known function names according to
their call probability?


…

> @lock@
…
> identifier lock = {spin_lock,…
>   …,mutex_lock_io};


Can such a function name list be also dynamically be determined?



…

> @@
>
> lock(\(&o.f@p\|&o.f@p[...]\),...)


Can the following SmPL code variant work also?

 lock(&o.
(f@p
|f@p[...]
)     , ...
     )



…
> @alias2@
…
> @@
>
> (
> return e;
> &
> return \(&o.f@p\|&o.f@p[...]\);
> )


Can the following SmPL code variant be helpful?

 return
(       e
&       &o.
(f@p
|f@p[...]
)
);


…

> @alias3@
> type t;
> t o;
> identifier f;
> expression ifn =~ "init";
> expression lfn =~ "lock";


How do you think about to apply more advanced regular expressions for
corresponding search patterns?



…

> @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;
> @@
…
>       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)


Can such a source code analysis approach be interpreted in the way
that internal data structures should be constructed for any special
knowledge representation from which final conclusions and advices
will be presented?

Regards,
Markus

Re: [cocci] Checking the usage of locks with SmPL

[Markus Elfring]

> @create4@
> identifier t,f;
> position pa;
> typedef spinlock_t;
> @@
>
> struct t {
>    ...
>    struct mutex f@pa[...];
>    ...
> }

* How much does the type definition matter for the referenced data structure
  in this SmPL rule?

* The shown source code search refers to an array as a member.
  Can such a selection be combined with a previous filter by using
  a corresponding SmPL disjunction?

* Would the application of iteration functionality become feasible
  for the discussed use case?

Regards,
Markus

Re: [cocci] Checking the usage of locks with SmPL

[Julia Lawall]

On Mon, 26 Sep 2022, Markus Elfring wrote:

> > @create4@
> > identifier t,f;
> > position pa;
> > typedef spinlock_t;
> > @@
> >
> > struct t {
> >    ...
> >    struct mutex f@pa[...];
> >    ...
> > }
>
> * How much does the type definition matter for the referenced data structure
>   in this SmPL rule?

No idea what this question means.

>
> * The shown source code search refers to an array as a member.
>   Can such a selection be combined with a previous filter by using
>   a corresponding SmPL disjunction?

No.  A disjunction will pick one case and match all possible matches of
this case.  Perhaps that could be improved, but that is the situation at
the moment.

> * Would the application of iteration functionality become feasible
>   for the discussed use case?

Not relevant.

julia

> Regards,
> Markus
>

Re: [cocci] Checking the usage of locks with SmPL

[Markus Elfring]

> > > @create4@
> > > identifier t,f;
> > > position pa;
> > > typedef spinlock_t;
> > > @@
> > >
> > > struct t {
> > >    ...
> > >    struct mutex f@pa[...];
> > >    ...
> > > }
> >
> > * How much does the type definition matter for the referenced data structure
> >   in this SmPL rule?
> 
> No idea what this question means.

May the metavariable “spinlock_t” be ommitted (when you are looking for mutexes here)?



> > * The shown source code search refers to an array as a member.
> >   Can such a selection be combined with a previous filter by using
> >   a corresponding SmPL disjunction?
> 
> No.  A disjunction will pick one case and match all possible matches of
> this case.  Perhaps that could be improved, but that is the situation at
> the moment.

Would it be nice to avoid duplicate SmPL code for the shown handling
of array and non-array variables?


> > * Would the application of iteration functionality become feasible
> >   for the discussed use case?
> 
> Not relevant.

Will it become possible to express repeated SmPL code by more convenient means?

Regards,
Markus

Re: [cocci] Checking the usage of locks with SmPL

[Markus Elfring]

> (* 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[...]\))


Can it matter to detect the usage of the following macros?
https://elixir.bootlin.com/linux/v6.0-rc7/source/include/linux/mutex.h#L108

* __MUTEX_INITIALIZER
* DEFINE_MUTEX


Regards,
Markus

Re: [cocci] Checking the usage of locks with SmPL

[Markus Elfring]

> Can the following SmPL code variant be helpful?
> 
>  return
> (       e
> &       &o.
> (f@p
> |f@p[...]
> )
> );

I tried also another SmPL code variant out.

@alias2@
typedef spinlock_t;
type t;
t o;
identifier f;
position p;
{spinlock_t,struct mutex} *e;
@@
 return
(       e
&       &o.f@p
?       [...]
);


Markus_Elfring@…:~/Aktivitäten> spatch --parse-cocci optional_array_member3.cocci
…
12: opt only allowed for the elements of a statement list


How will the chances evolve to reconsider mentioned software limitations any more?

How does the source code search approach fit together for a selected pointer
and the array access for a data structure member at the same place
(according to the SmPL conjunction)?

Regards,
Markus

Re: [cocci] Checking the usage of locks with SmPL

[Markus Elfring]

> @lock@
> type t;
> t o;
> identifier f;
> identifier lock = {spin_lock,…
> …,mutex_lock_io};
> position p;
> @@
>
> lock(\(&o.f@p\|&o.f@p[...]\),...)


I got the impression that you demonstrate a special application of
the metavariable kind “type” here.
(I imagine that addresses would be determined from data structure members
according to passed identifiers.)
* How do you think about to explain such an implementation detail a bit more?
* Can the SmPL manual be adjusted accordingly?

Regards,
Markus

Re: [cocci] Checking the usage of locks with SmPL

[Julia Lawall]

[-- Attachment #1: Type: text/plain, Size: 638 bytes --]



On Wed, 28 Sep 2022, Markus Elfring wrote:

> > @lock@
> > type t;
> > t o;
> > identifier f;
> > identifier lock = {spin_lock,…
> > …,mutex_lock_io};
> > position p;
> > @@
> >
> > lock(\(&o.f@p\|&o.f@p[...]\),...)
>
>
> I got the impression that you demonstrate a special application of
> the metavariable kind “type” here.
> (I imagine that addresses would be determined from data structure members
> according to passed identifiers.)
> * How do you think about to explain such an implementation detail a bit more?
> * Can the SmPL manual be adjusted accordingly?

t is a metavariable that gats bound to the type of o.

julia

Re: [cocci] Checking the usage of locks with SmPL

[Markus Elfring]

> t is a metavariable that gats bound to the type of o.


I would use the kind “identifier” for the metavariable “o” which is connected
to a known data type.
I would appreciate if the usage of your SmPL code can become clearer.

Regards,
Markus

Re: [cocci] Checking the usage of locks with SmPL

[Julia Lawall]

[-- Attachment #1: Type: text/plain, Size: 656 bytes --]



On Wed, 28 Sep 2022, Markus Elfring wrote:

> > t is a metavariable that gats bound to the type of o.
>
>
> I would use the kind “identifier” for the metavariable “o” which is connected
> to a known data type.
> I would appreciate if the usage of your SmPL code can become clearer.

In SmPL, if you want to declare a metavariable that matches an expression
of a certain type, you don't have to write the word expression.  For
example, you can write

int x;

and then x will maych any expression of type int.

And if you write

t x;

then x will match any expression of type t, t being another metavariable
that will get bound to that type.

julia

Re: [cocci] Checking the usage of locks with SmPL

[Markus Elfring]

> > > t is a metavariable that gats bound to the type of o.
> >
> >
> > I would use the kind “identifier” for the metavariable “o” which is connected
> > to a known data type.
> > I would appreciate if the usage of your SmPL code can become clearer.
> 
> In SmPL, if you want to declare a metavariable that matches an expression
> of a certain type, you don't have to write the word expression.

* Would you like to restrict the source code search to compound data types?

* How do you think about to check if there are differences in the software
  run time characteristics for the application of the metavariable kinds
  “identifier” and “type”?

Regards,
Markus

Re: [cocci] Checking the usage of locks with SmPL

[Julia Lawall]

[-- Attachment #1: Type: text/plain, Size: 1072 bytes --]



On Thu, 29 Sep 2022, Markus Elfring wrote:

> > > > t is a metavariable that gats bound to the type of o.
> > >
> > >
> > > I would use the kind “identifier” for the metavariable “o” which is connected
> > > to a known data type.
> > > I would appreciate if the usage of your SmPL code can become clearer.
> >
> > In SmPL, if you want to declare a metavariable that matches an expression
> > of a certain type, you don't have to write the word expression.
>
> * Would you like to restrict the source code search to compound data types?
>
> * How do you think about to check if there are differences in the software
>   run time characteristics for the application of the metavariable kinds
>   “identifier” and “type”?

Huh?  Why would I want to use identifier?  First an identifier doesn't
have a type, it's just a sequence of characters.  So I would not know the
type of the expression, which is necessary for matching up the various
uses of the locks, and second the thing in the matched position is not
always an identifier, as in &a->b->lock.

julia

Re: [cocci] Checking the usage of locks with SmPL

[Markus Elfring]

> > > In SmPL, if you want to declare a metavariable that matches an expression
> > > of a certain type, you don't have to write the word expression.
> >
> > * Would you like to restrict the source code search to compound data types?
> >
> > * How do you think about to check if there are differences in the software
> >   run time characteristics for the application of the metavariable kinds
> >   “identifier” and “type”?
> 
> Huh?  Why would I want to use identifier?

I interpret the SmPL rule “lock” in the way that source code should be found
that fits to calls of selected macros (or functions) which get addresses passed
from data structure members.
The address determination would usually start with the evaluation of a variable name,
wouldn't it?


> First an identifier doesn't have a type, it's just a sequence of characters.

Can the view be appropriate that identifiers have got the data type “char[]”
(or “std::string”)?
They refer to additional information.


> So I would not know the type of the expression,

Maybe not directly.

The effective data type of expressions can eventually be determined in ways
which are supported by available compilers.

It seems that we usually expect also that appropriate pointers are passed
to selected macros (or functions).


> which is necessary for matching up the various uses of the locks,

How would you like to improve the desired scope (or name) resolution further?
https://en.cppreference.com/w/c/language/scope


> and second the thing in the matched position is not always an identifier,
> as in &a->b->lock.

How would you call the item “a” then according to such an expression example?
Which terminology would you prefer instead?

Regards,
Markus

Re: [cocci] Checking the usage of locks with SmPL

[Julia Lawall]

[-- Attachment #1: Type: text/plain, Size: 2453 bytes --]



On Thu, 29 Sep 2022, Markus Elfring wrote:

> > > > In SmPL, if you want to declare a metavariable that matches an expression
> > > > of a certain type, you don't have to write the word expression.
> > >
> > > * Would you like to restrict the source code search to compound data types?
> > >
> > > * How do you think about to check if there are differences in the software
> > >   run time characteristics for the application of the metavariable kinds
> > >   “identifier” and “type”?
> >
> > Huh?  Why would I want to use identifier?
>
> I interpret the SmPL rule “lock” in the way that source code should be found
> that fits to calls of selected macros (or functions) which get addresses passed
> from data structure members.
> The address determination would usually start with the evaluation of a variable name,
> wouldn't it?

Sure, but in &a->b->xyz, the type of a is useless in figuring out whether
this is a pointer to a lock, and in relating this expression to other
expressions, perhaps with the form &q->xyz that may refer to the same
lock.

So we dont' care about the thing that is immediately to the right of the
&.  We care about the complete thing that is between the & and the ->xyz.
And that thing is an expression.

>
> > First an identifier doesn't have a type, it's just a sequence of characters.
>
> Can the view be appropriate that identifiers have got the data type “char[]”
> (or “std::string”)?
> They refer to additional information.

In Coccinelle those can be matched as expressions or as idexpressions (an
expression that if required to have the form of identifier).

An expression is a piece of code that has a value.  Hence an expression
has a type that describes that possible value.

An identifier is a sequence of characters.  Some identifiers are
expressions, but not all.

> How would you like to improve the desired scope (or name) resolution further?
> https://en.cppreference.com/w/c/language/scope

What is wrong with it as it is now?  The type inference of Coccinelle
follows the scope rules of C (like any type inferencer for any language).

> > and second the thing in the matched position is not always an identifier,
> > as in &a->b->lock.
>
> How would you call the item “a” then according to such an expression example?
> Which terminology would you prefer instead?

a is an identifier.  It is also an expression.  But is not not useful in
this semantic patch in any case.

julia

Re: [cocci] Checking the usage of locks with SmPL

[Markus Elfring]

> > > Huh?  Why would I want to use identifier?
> >
> > I interpret the SmPL rule “lock” in the way that source code should be found
> > that fits to calls of selected macros (or functions) which get addresses passed
> > from data structure members.
> > The address determination would usually start with the evaluation of a variable name,
> > wouldn't it?
> 
> Sure, but in &a->b->xyz, the type of a is useless

The item “a” can be used for a member access operation.


> in figuring out whether this is a pointer to a lock,

Such information should be provided by the identifier “xyz” (at the end
of discussed expression variants), shouldn't it?


> and in relating this expression to other expressions, perhaps with the form
> &q->xyz that may refer to the same lock.

I find the indicated concern unclear.


> So we dont' care about the thing that is immediately to the right of the &.

I got an other impression according to the proper selection of a corresponding
source code filter.


> We care about the complete thing that is between the & and the ->xyz.
> And that thing is an expression.

I agree to this view.


> > How would you like to improve the desired scope (or name) resolution further?
> > https://en.cppreference.com/w/c/language/scope
> 
> What is wrong with it as it is now?

I got the impression that the representation of corresponding scopes is still unclear.


> The type inference of Coccinelle follows the scope rules of C
> (like any type inferencer for any language).

This can be.

Do discussed data structures (like simpler source code search approaches
or the used OCaml data type “Hashtbl”) trigger other software development views?


> > > and second the thing in the matched position is not always an identifier,
> > > as in &a->b->lock.
> >
> > How would you call the item “a” then according to such an expression example?
> > Which terminology would you prefer instead?
> 
> a is an identifier.  It is also an expression.

Would you find the SmPL term “idexpression” more appropriate then?


> But is not not useful in this semantic patch in any case.

I find the double negation confusing in this wording.

Regards,
Markus

Re: [cocci] Checking the usage of locks with SmPL

[Julia Lawall]

[-- Attachment #1: Type: text/plain, Size: 2634 bytes --]



On Thu, 29 Sep 2022, Markus Elfring wrote:

> > > > Huh?  Why would I want to use identifier?
> > >
> > > I interpret the SmPL rule “lock” in the way that source code should be found
> > > that fits to calls of selected macros (or functions) which get addresses passed
> > > from data structure members.
> > > The address determination would usually start with the evaluation of a variable name,
> > > wouldn't it?
> >
> > Sure, but in &a->b->xyz, the type of a is useless
>
> The item “a” can be used for a member access operation.

Anything can be used for anything, but it's not useful in this context.
We are interested in the object a->b which has a field called lock.

> > in figuring out whether this is a pointer to a lock,
>
> Such information should be provided by the identifier “xyz” (at the end
> of discussed expression variants), shouldn't it?

No, xyz is just an offset from the top of a structure.  To figure out what
type the value at that offset has, you need to find the associated
structure.  So you need the a->b part.

> > and in relating this expression to other expressions, perhaps with the form
> > &q->xyz that may refer to the same lock.
>
> I find the indicated concern unclear.

A single object could be called a-> b or it could be called q, eg in
different parts of the source code.  We don't care what it's called.  We
care what its type is.

> > > How would you like to improve the desired scope (or name) resolution further?
> > > https://en.cppreference.com/w/c/language/scope
> >
> > What is wrong with it as it is now?
>
> I got the impression that the representation of corresponding scopes is still unclear.

There is no real representation of scopes in SmPL.  But the type inference
does not rely on what is expressed by the semantic patch.  It just looks
at the C source code available and does the best it can.

> > > > and second the thing in the matched position is not always an identifier,
> > > > as in &a->b->lock.
> > >
> > > How would you call the item “a” then according to such an expression example?
> > > Which terminology would you prefer instead?
> >
> > a is an identifier.  It is also an expression.
>
> Would you find the SmPL term “idexpression” more appropriate then?

In the above expression, a can be matched by a metavariable that is
declared as identifier, expression or idexpression.  And if the type of a
is indicated in the metavariable declaration, the word expression can be
omitted.

> > But is not not useful in this semantic patch in any case.
>
> I find the double negation confusing in this wording.

The second "not" was a typo.

julia

Re: [cocci] Checking the usage of locks with SmPL

[Markus Elfring]

> > > > How would you like to improve the desired scope (or name) resolution further?
> > > > https://en.cppreference.com/w/c/language/scope
> > >
> > > What is wrong with it as it is now?
> >
> > I got the impression that the representation of corresponding scopes is still unclear.
>
> There is no real representation of scopes in SmPL.

Thanks for this information.

* Will it trigger further development considerations?

* Can the handling of scopes be an essential functionality for safe source code analyses?


> But the type inference does not rely on what is expressed by the semantic patch.

Such a feedback is promising.


> It just looks at the C source code available and does the best it can.

Corresponding data processing approaches will evolve further, won't they?

Regards,
Markus

Re: [cocci] Checking explanations for SmPL functionality

[Markus Elfring]

…
> (* check for aliases or non-standard uses *)
>
> @alias1@
> type t;
> t o;

…


I got the impression that such a code specification is not completely explained
in the documentation for the semantic patch language so far.
https://gitlab.inria.fr/coccinelle/coccinelle/-/blob/19454bc12f6f8cc0a7a6091edb28e8a2ca4518c2/docs/manual/cocci_syntax.tex#L199

Which metavariable declarations may be started with a metavariable name?

Regards,
Markus

Re: [cocci] Checking explanations for SmPL functionality

[Julia Lawall]

[-- Attachment #1: Type: text/plain, Size: 838 bytes --]



On Mon, 3 Oct 2022, Markus Elfring wrote:

> …
> > (* check for aliases or non-standard uses *)
> >
> > @alias1@
> > type t;
> > t o;
>
> …
>
>
> I got the impression that such a code specification is not completely explained
> in the documentation for the semantic patch language so far.
> https://gitlab.inria.fr/coccinelle/coccinelle/-/blob/19454bc12f6f8cc0a7a6091edb28e8a2ca4518c2/docs/manual/cocci_syntax.tex#L199
>
> Which metavariable declarations may be started with a metavariable name?

This is what the documentation says currently:

It is possible to only match expressions of a specific \NT{ctype} or a set
of them with a pointer level using {\tt *} by writing these instead of the
{\bf expression} designator pattern.

It seems that that should be changed to type rather than ctype.

julia



>
> Regards,
> Markus
>
>

Re: [cocci] Checking explanations for SmPL functionality

[Markus Elfring]

>> https://gitlab.inria.fr/coccinelle/coccinelle/-/blob/19454bc12f6f8cc0a7a6091edb28e8a2ca4518c2/docs/manual/cocci_syntax.tex#L199
>>
>> Which metavariable declarations may be started with a metavariable name?
> This is what the documentation says currently:
>
> It is possible to only match expressions of a specific \NT{ctype} or a set
> of them with a pointer level using {\tt *} by writing these instead of the
> {\bf expression} designator pattern.
>
> It seems that that should be changed to type rather than ctype.

Would you like to add any more helpful explanations to the manual for users
of your sophisticated software?

Regards,
Markus

Re: [cocci] Checking explanations for SmPL functionality

[Markus Elfring]

>> https://gitlab.inria.fr/coccinelle/coccinelle/-/blob/19454bc12f6f8cc0a7a6091edb28e8a2ca4518c2/docs/manual/cocci_syntax.tex#L199
>>
>> Which metavariable declarations may be started with a metavariable name?
> This is what the documentation says currently:
>
> It is possible to only match expressions of a specific \NT{ctype} or a set
> of them with a pointer level using {\tt *} by writing these instead of the
> {\bf expression} designator pattern.
>
> It seems that that should be changed to type rather than ctype.

I find your commit (from 5 hours ago) improvable.
https://gitlab.inria.fr/coccinelle/coccinelle/-/commit/7cf3e705f8fb5c013cdb10a8e5c05c22938b2842

Will further adjustments become helpful for a better description also for
the grammar of the semantic patch language besides more valuable explanations
in the user manual?
Are additional case distinctions relevant?

Regards,
Markus