Re: [PATCH] coccinelle: tests: unsigned value cannot be lesser than zero

Re: [PATCH] coccinelle: tests: unsigned value cannot be lesser than zero

[SF Markus Elfring]

> +@r depends on context || org || report@
> +position p;
> +typedef u8, u16, u32, u64;

Can the involved data types be restricted for unsigned types for such
a source code analysis in a more general way?


> +{unsigned char, unsigned short int, unsigned int, unsigned long, unsigned long long, size_t, u8, u16, u32, u64} v;
> +@@
> +
> +(
> +*v@p < 0
> +|
> +*v@p >= 0
> +)

How do you think about to use the following SmPL wording instead?

 v@p
(
*< 0
|
*<= 0
)

Regards,
Markus

Re: [PATCH] coccinelle: tests: unsigned value cannot be lesser than zero

[Julia Lawall]

On Tue, 15 Sep 2015, SF Markus Elfring wrote:

> > +@r depends on context || org || report@
> > +position p;
> > +typedef u8, u16, u32, u64;
>
> Can the involved data types be restricted for unsigned types for such
> a source code analysis in a more general way?
>
>
> > +{unsigned char, unsigned short int, unsigned int, unsigned long, unsigned long long, size_t, u8, u16, u32, u64} v;
> > +@@
> > +
> > +(
> > +*v@p < 0
> > +|
> > +*v@p >= 0
> > +)
>
> How do you think about to use the following SmPL wording instead?
>
>  v@p
> (
> *< 0
> |
> *<= 0
> )

It does not, and is not intended to, work.  The branches of a disjunction
should be complete expressions.

julia

Re: [PATCH] coccinelle: tests: unsigned value cannot be lesser than zero

[SF Markus Elfring]

>>  v@p
>> (
>> *< 0
>> |
>> *<= 0
>> )
> 
> It does not, and is not intended to, work.  The branches of a disjunction
> should be complete expressions.

Will the following SmPL approach be more appropriate then?

(
*v@p < 0
|
*v@p <= 0
)

Regards,
Markus

Re: [PATCH] coccinelle: tests: unsigned value cannot be lesser than zero

[Julia Lawall]

On Tue, 15 Sep 2015, SF Markus Elfring wrote:

> >>  v@p
> >> (
> >> *< 0
> >> |
> >> *<= 0
> >> )
> >
> > It does not, and is not intended to, work.  The branches of a disjunction
> > should be complete expressions.
>
> Will the following SmPL approach be more appropriate then?
>
> (
> *v@p < 0
> |
> *v@p <= 0
> )

Actually, all of

v < 0 (never true)
v <= 0 (same as v = 0)
v >= 0 (always true)

would seem to merit attention.  Andrzej, what do you think?

julia


>
> Regards,
> Markus
> --
> To unsubscribe from this list: send the line "unsubscribe kernel-janitors" in
> the body of a message to majordomo@vger.kernel.org
> More majordomo info at  http://vger.kernel.org/majordomo-info.html
>

Re: [PATCH] coccinelle: tests: unsigned value cannot be lesser than zero

[Andrzej Hajda]

On 09/15/2015 03:31 PM, Julia Lawall wrote:
> On Tue, 15 Sep 2015, SF Markus Elfring wrote:
>
>>>>  v@p
>>>> (
>>>> *< 0
>>>> |
>>>> *<= 0
>>>> )
>>> It does not, and is not intended to, work.  The branches of a disjunction
>>> should be complete expressions.
>> Will the following SmPL approach be more appropriate then?
>>
>> (
>> *v@p < 0
>> |
>> *v@p <= 0
>> )
> Actually, all of
>
> v < 0 (never true)
> v <= 0 (same as v = 0)
> v >= 0 (always true)
>
> would seem to merit attention.  Andrzej, what do you think?

You are right, the 2nd case should be also addressed,
such code is misleading.
I will prepare then 2nd version of the patch.

Regards
Andrzej

>
> julia
>
>
>> Regards,
>> Markus
>> --
>> To unsubscribe from this list: send the line "unsubscribe kernel-janitors" in
>> the body of a message to majordomo@vger.kernel.org
>> More majordomo info at  http://vger.kernel.org/majordomo-info.html
>>

Re: [PATCH] coccinelle: tests: unsigned value cannot be lesser than zero

[Julia Lawall]

On Tue, 15 Sep 2015, Andrzej Hajda wrote:

> On 09/15/2015 03:31 PM, Julia Lawall wrote:
> > On Tue, 15 Sep 2015, SF Markus Elfring wrote:
> >
> >>>>  v@p
> >>>> (
> >>>> *< 0
> >>>> |
> >>>> *<= 0
> >>>> )
> >>> It does not, and is not intended to, work.  The branches of a disjunction
> >>> should be complete expressions.
> >> Will the following SmPL approach be more appropriate then?
> >>
> >> (
> >> *v@p < 0
> >> |
> >> *v@p <= 0
> >> )
> > Actually, all of
> >
> > v < 0 (never true)
> > v <= 0 (same as v = 0)
> > v >= 0 (always true)
> >
> > would seem to merit attention.  Andrzej, what do you think?
>
> You are right, the 2nd case should be also addressed,
> such code is misleading.
> I will prepare then 2nd version of the patch.

It could be reasonable to change the options to --all-includes?  Although
it could be somewhat slow.

julia

>
> Regards
> Andrzej
>
> >
> > julia
> >
> >
> >> Regards,
> >> Markus
> >> --
> >> To unsubscribe from this list: send the line "unsubscribe kernel-janitors" in
> >> the body of a message to majordomo@vger.kernel.org
> >> More majordomo info at  http://vger.kernel.org/majordomo-info.html
> >>
>
>

Re: [PATCH] coccinelle: tests: unsigned value cannot be lesser than zero

[Andrzej Hajda]

On 09/15/2015 03:57 PM, Julia Lawall wrote:
> 
> 
> On Tue, 15 Sep 2015, Andrzej Hajda wrote:
> 
>> On 09/15/2015 03:31 PM, Julia Lawall wrote:
>>> On Tue, 15 Sep 2015, SF Markus Elfring wrote:
>>>
>>>>>>  v@p
>>>>>> (
>>>>>> *< 0
>>>>>> |
>>>>>> *<= 0
>>>>>> )
>>>>> It does not, and is not intended to, work.  The branches of a disjunction
>>>>> should be complete expressions.
>>>> Will the following SmPL approach be more appropriate then?
>>>>
>>>> (
>>>> *v@p < 0
>>>> |
>>>> *v@p <= 0
>>>> )
>>> Actually, all of
>>>
>>> v < 0 (never true)
>>> v <= 0 (same as v = 0)
>>> v >= 0 (always true)
>>>
>>> would seem to merit attention.  Andrzej, what do you think?
>>
>> You are right, the 2nd case should be also addressed,
>> such code is misleading.
>> I will prepare then 2nd version of the patch.
> 
> It could be reasonable to change the options to --all-includes?  Although
> it could be somewhat slow.

I have tested the patch with 'v <= 0', it spotted hundreds places with this
check. It seems to be quite common practice to use such checks with counters,
iterators, quantities, range checking. In fact it is negation of 'v > 0' which
seems to be acceptable even if it really means 'v != 0'. So maybe we should not
warn about it? What do you think?

On the other side it spotted also real bugs, but maybe I can make separate, more
specific test for such cases.

Regards
Andrzej

> 
> julia
> 
>>
>> Regards
>> Andrzej
>>
>>>
>>> julia
>>>
>>>
>>>> Regards,
>>>> Markus
>>>> --
>>>> To unsubscribe from this list: send the line "unsubscribe kernel-janitors" in
>>>> the body of a message to majordomo@vger.kernel.org
>>>> More majordomo info at  http://vger.kernel.org/majordomo-info.html
>>>>
>>
>>
> --
> To unsubscribe from this list: send the line "unsubscribe kernel-janitors" in
> the body of a message to majordomo@vger.kernel.org
> More majordomo info at  http://vger.kernel.org/majordomo-info.html
> 

Re: [PATCH] coccinelle: tests: unsigned value cannot be lesser than zero

[Julia Lawall]

On Wed, 16 Sep 2015, Andrzej Hajda wrote:

> On 09/15/2015 03:57 PM, Julia Lawall wrote:
> >
> >
> > On Tue, 15 Sep 2015, Andrzej Hajda wrote:
> >
> >> On 09/15/2015 03:31 PM, Julia Lawall wrote:
> >>> On Tue, 15 Sep 2015, SF Markus Elfring wrote:
> >>>
> >>>>>>  v@p
> >>>>>> (
> >>>>>> *< 0
> >>>>>> |
> >>>>>> *<= 0
> >>>>>> )
> >>>>> It does not, and is not intended to, work.  The branches of a disjunction
> >>>>> should be complete expressions.
> >>>> Will the following SmPL approach be more appropriate then?
> >>>>
> >>>> (
> >>>> *v@p < 0
> >>>> |
> >>>> *v@p <= 0
> >>>> )
> >>> Actually, all of
> >>>
> >>> v < 0 (never true)
> >>> v <= 0 (same as v = 0)
> >>> v >= 0 (always true)
> >>>
> >>> would seem to merit attention.  Andrzej, what do you think?
> >>
> >> You are right, the 2nd case should be also addressed,
> >> such code is misleading.
> >> I will prepare then 2nd version of the patch.
> >
> > It could be reasonable to change the options to --all-includes?  Although
> > it could be somewhat slow.
>
> I have tested the patch with 'v <= 0', it spotted hundreds places with this
> check. It seems to be quite common practice to use such checks with counters,
> iterators, quantities, range checking. In fact it is negation of 'v > 0' which
> seems to be acceptable even if it really means 'v != 0'. So maybe we should not
> warn about it? What do you think?

It seems a bit sloppy, but since the test does have some meaning, maybe it
is OK.

> On the other side it spotted also real bugs, but maybe I can make separate, more
> specific test for such cases.

OK, thanks.

julia

Re: [PATCH v2] coccinelle: tests: unsigned value cannot be lesser than zero

[SF Markus Elfring]

> As we discussed earlier I have dropped idea of adding v <= 0 as it is widely
> used in checking ranges, counters, quantities.

I find that such a design decision will need more fine-tuning of the suggested
small SmPL script.


> +@r depends on context || org || report@
> +position p;
> +typedef u8, u16, u32, u64;
> +{unsigned char, unsigned short int, unsigned int, unsigned long, unsigned long long, size_t, u8, u16, u32, u64} v;

Is it eventually needed to mention the key word "int" also together with the "long" data types?


> +@@
> +
> +(
> +*v@p < 0
> +|
> +*v@p >= 0
> +)

How do you think about to split this SmPL rule so that corresponding warning
messages will really fit?

Regards,
Markus

Re: [PATCH] coccinelle: tests: unsigned value cannot be lesser than zero

[Andrzej Hajda]

On 09/15/2015 03:01 PM, SF Markus Elfring wrote:
>> +@r depends on context || org || report@
>> +position p;
>> +typedef u8, u16, u32, u64;
> Can the involved data types be restricted for unsigned types for such
> a source code analysis in a more general way?

I am not sure if I understand correctly. If you think about removing all u*
typedefs it
will result in omitting u* related comparisons, unless you use
--recursive-includes option.
Another solution is to add '--include include/asm-generic/int-ll64.h' to kbuild,
surprisingly
this header file is common for all architectures :)

Regards
Andrzej

>
>
>> +{unsigned char, unsigned short int, unsigned int, unsigned long, unsigned long long, size_t, u8, u16, u32, u64} v;
>> +@@
>> +
>> +(
>> +*v@p < 0
>> +|
>> +*v@p >= 0
>> +)
> How do you think about to use the following SmPL wording instead?
>
>  v@p
> (
> *< 0
> |
> *<= 0
> )
>
> Regards,
> Markus
>

Re: [PATCH] coccinelle: tests: unsigned value cannot be lesser than zero

[SF Markus Elfring]

> If you think about removing all u* typedefs

I became interested in the use case to consider more type definitions
besides the ones which should usually be handled for Linux source files.


> it will result in omitting u* related comparisons,
> unless you use --recursive-includes option.

How do you think about to make this source code analysis parameter configurable?


>>> +{unsigned char, unsigned short int, unsigned int, unsigned long, unsigned long long, size_t, u8, u16, u32, u64} v;

How does the data type "size_t" fit into the suggested SmPL approach?

Would you like to reuse your approach for checking of more software eventually?

Regards,
Markus

Re: [Cocci] [PATCH] coccinelle: tests: unsigned value cannot be lesser than zero

[Julia Lawall]

On Tue, 15 Sep 2015, SF Markus Elfring wrote:

> > If you think about removing all u* typedefs
>
> I became interested in the use case to consider more type definitions
> besides the ones which should usually be handled for Linux source files.
>
>
> > it will result in omitting u* related comparisons,
> > unless you use --recursive-includes option.
>
> How do you think about to make this source code analysis parameter configurable?

What parameter are you referring to?  --recursive-includes is already a
parameter.

> >>> +{unsigned char, unsigned short int, unsigned int, unsigned long, unsigned long long, size_t, u8, u16, u32, u64} v;
>
> How does the data type "size_t" fit into the suggested SmPL approach?

size_t is also unsigned.

> Would you like to reuse your approach for checking of more software
> eventually?

He is proposing a semantic patch for inclusion in the Linux kernel source
code, so it is not really necessary to consider types other than those
used by the Linux kernel.  People can modify the semantic patch if they
want for other uses.

julia

Re: [Cocci] [PATCH] coccinelle: tests: unsigned value cannot be lesser than zero

[SF Markus Elfring]

> --recursive-includes is already a parameter.

I am unsure if its effect on source code analysis speed will matter here.


> size_t is also unsigned.

Will such a specification work also without an explicit SmPL typedef?

Regards,
Markus

Re: [PATCH] coccinelle: tests: unsigned value cannot be lesser than zero

[Julia Lawall]

 >> +{unsigned char, unsigned short int, unsigned int, unsigned long, unsigned long long, size_t, u8, u16, u32, u64} v;

How about adding bool?  I don't currently find any problems with it, but
perhaps some could arise.

julia


> >> +@@
> >> +
> >> +(
> >> +*v@p < 0
> >> +|
> >> +*v@p >= 0
> >> +)
> > How do you think about to use the following SmPL wording instead?
> >
> >  v@p
> > (
> > *< 0
> > |
> > *<= 0
> > )
> >
> > Regards,
> > Markus
> >
> 
> --
> To unsubscribe from this list: send the line "unsubscribe kernel-janitors" in
> the body of a message to majordomo@vger.kernel.org
> More majordomo info at  http://vger.kernel.org/majordomo-info.html
> 

[PATCH v3] coccinelle: tests: unsigned value cannot be lesser than zero

[Andrzej Hajda]

Code comparing unsigned variables with zero using operators < or >= does not
make sense. It is always false or true, respectively. However, its presence
often indicates bugs in the code.
gcc can detect it also using -Wtype-limits switch, but it warns also in correct
cases, making too much noise.

Signed-off-by: Andrzej Hajda <a.hajda@samsung.com>
Acked-by: Julia Lawall <julia.lawall@lip6.fr>
---
v3: added bool type
v2: added --all-includes option
---
 .../tests/unsigned_lesser_than_zero.cocci          | 37 ++++++++++++++++++++++
 1 file changed, 37 insertions(+)
 create mode 100644 scripts/coccinelle/tests/unsigned_lesser_than_zero.cocci

diff --git a/scripts/coccinelle/tests/unsigned_lesser_than_zero.cocci b/scripts/coccinelle/tests/unsigned_lesser_than_zero.cocci
new file mode 100644
index 0000000..70e71c8
--- /dev/null
+++ b/scripts/coccinelle/tests/unsigned_lesser_than_zero.cocci
@@ -0,0 +1,37 @@
+/// Unsigned variables cannot be lesser than zero. Presence of such checks
+/// can indicate incorrect variable type or just unnecessary code.
+///
+// Confidence: High
+// Copyright: (C) 2015 Andrzej Hajda, Samsung Electronics Co., Ltd. GPLv2.
+// URL: http://coccinelle.lip6.fr/
+// Options: --include-headers --all-includes
+
+virtual context
+virtual org
+virtual report
+
+@r depends on context || org || report@
+position p;
+typedef bool, u8, u16, u32, u64;
+{unsigned char, unsigned short int, unsigned int, unsigned long, unsigned long long, size_t, bool, u8, u16, u32, u64} v;
+@@
+
+(
+*v@p < 0
+|
+*v@p >= 0
+)
+
+@script:python depends on org@
+p << r.p;
+@@
+
+msg = "WARNING: Unsigned value cannot be lesser than zero"
+coccilib.org.print_todo(p[0], msg)
+
+@script:python depends on report@
+p << r.p;
+@@
+
+msg = "WARNING: Unsigned value cannot be lesser than zero"
+coccilib.report.print_report(p[0], msg)
-- 
1.9.1

Re: [PATCH v3] coccinelle: tests: unsigned value cannot be lesser than zero

[SF Markus Elfring]

> v3: added bool type

I would appreciate a bit more feedback for my concerns around your
evolving approach.
* Reuse of "long int"?
* Splitting of the suggested SmPL rule so that each source code check
will be connected with appropriate warning messages.

Will any more fine-tuning be useful?

Regards,
Markus

Re: [PATCH v3] coccinelle: tests: unsigned value cannot be lesser than zero

[Andrzej Hajda]

On 09/21/2015 03:02 PM, SF Markus Elfring wrote:
>> v3: added bool type
> I would appreciate a bit more feedback for my concerns around your
> evolving approach.

Ups, I have missed your email.

> * Reuse of "long int"?
If you mean adding int to 'unsigned long [long]' types, it does not work.
For some reason it works only without adding int after long.

> * Splitting of the suggested SmPL rule so that each source code check
> will be connected with appropriate warning messages.

Personally I prefer one message as it is more compact and
fits quite well in both cases, but I have no strong fillings with separate
message for each case.

>
> Will any more fine-tuning be useful?
Could you elaborate it.

Regards
Andrzej

>
> Regards,
> Markus
>

Re: [PATCH v3] coccinelle: tests: unsigned value cannot be lesser than zero

[SF Markus Elfring]

>> * Reuse of "long int"?
> If you mean adding int to 'unsigned long [long]' types, it does not work.

I am surprised.


> For some reason it works only without adding int after long.

The  Coccinelle software should support the term "generic_ctype" from
the SmPL grammar so far, shouldn't it?
http://coccinelle.lip6.fr/docs/main_grammar005.html#ctype


>> * Splitting of the suggested SmPL rule so that each source code check
>> will be connected with appropriate warning messages.
> Personally I prefer one message as it is more compact

It might look convenient to combine a few source code checks.


> and fits quite well in both cases,

I got an other impression.


> but I have no strong fillings with separate message for each case.

* v@p < 0
  Find places where this condition will always be false.

*v@p >= 0
  Find places where this condition will always be true.


Will it help to distinguish these special cases also in your SmPL script
strictly?

Regards,
Markus

Re: [PATCH v3] coccinelle: tests: unsigned value cannot be lesser than zero

[SF Markus Elfring]

> If you mean adding int to 'unsigned long [long]' types, it does not work.
> For some reason it works only without adding int after long.

Do you get any error message for this SmPL approach?
With which source files do you try the extended SmPL script out?

Regards,
Markus

Re: [PATCH v3] coccinelle: tests: unsigned value cannot be lesser than zero

[Andrzej Hajda]

On 09/22/2015 05:27 PM, SF Markus Elfring wrote:
>> If you mean adding int to 'unsigned long [long]' types, it does not work.
>> For some reason it works only without adding int after long.
> Do you get any error message for this SmPL approach?
> With which source files do you try the extended SmPL script out?
>
> Regards,
> Markus
>
No, spatch just does not find everything it should. Sample below:
--- test.cocci
virtual context

@r depends on context@
{unsigned char, unsigned short int, unsigned int, unsigned long int, unsigned
long long, size_t} v;
@@

*v
--- test.c
void f()
{
    unsigned long ul;
    unsigned long int uli;
    unsigned long long ull;
    unsigned long long int ulli;

    ul;
    uli;
    ull;
    ulli;
}
---
In the example above spatch finds ull, ulli, but not ul and uli.
If you add int to unsigned long long, it won't find anything.

Regards
Andrzej

Re: [PATCH v3] coccinelle: tests: unsigned value cannot be lesser than zero

[SF Markus Elfring]

> In the example above spatch finds ull, ulli, but not ul and uli.
> If you add int to unsigned long long, it won't find anything.

I suggest to take another look at the use of type modifiers
in the semantic patch language. It seems that it matters occasionally
to specify them explicitly.

How do you think about to reuse a SmPL script like the following?


@find_unsigned@
typedef _Bool, bool, u8, u16, u32, u64;
{
unsigned,
unsigned char,
unsigned int,
unsigned short,
unsigned short int,
unsigned long,
unsigned long int,
unsigned long long,
unsigned long long int,
size_t,
_Bool,
bool,
u8,
u16,
u32,
u64
} var;
@@
*var


Regards,
Markus