On Fri, 23 Sep 2022, Markus Elfring wrote:
> >>> +@r3@
> >>> +identifier s, fld;
> >>> +position p != {r2.p};
> >>> +@@
> >>> +
> >>> +struct s {
> >>> + ...
> >>> + struct mutex fld@p;
> >>> + ...
> >>> +};
> >>
> >> How many mutexes (or spin locks) should be initialised before further data
> >> processing can be safely performed with corresponding structures?
> > I tried the semantic patch on this file:
> >
> > struct s {
> > struct mutex fld;
> > };
> >
> > int main () {
> > struct s *mm;
> > mm = kmalloc();
> > mutex_lock(&mm->fld);
> > }
> >
> > and it reported the expected error message.
>
>
> This test result might be nice.
>
>
> > So what exactly is the concern, Markus?
>
>
> I just suggest to check once more if it would be really required to determine
> the position for a data structure member twice (as proposed by the SmPL rules
> “r2” and “r3”).
>
> Would you like to compare the data processing for a SmPL code variant
> like the following?
>
> @find_member@
> identifier s1, s2, f;
> position p;
> @@
> struct s1
> {
> ...
> struct s2 f@p;
> ...
> };
>
> @show_member@
> identifier s1, s2, f;
> position p != find_member.p;
> @@
> struct s1
> {
> ...
> *struct s2 f@p;
> ...
> };
>
>
> # How do you think about the handling of multiple members within data structures?
There should be no problem with this.
> # How much does it matter here that curly brackets are used for a proposed SmPL constraint?
I have no idea what "How much does it matter" mean. {} are used because
that's how struct types are declared.
>
>
> I got another development concern for the presented algorithm.
> Why is a data initialisation function call searched in the first SmPL rule at all?
Because he wants to find the fields for which mutex_init is already called
and to not report messages for them. That is the whole point of the
semantic patch.
julia
>
> I imagine that potentially missing function calls can be determined also
> by other approaches.
>
> Regards,
> Markus
>
>
