xen-analysis ECLAIR support

xen-analysis ECLAIR support

[Stefano Stabellini]

Hi Luca,

We are looking into adding ECLAIR support for xen-analysis so that we
can use the SAF-n-safe tags also with ECLAIR.

One question that came up is about multi-line statements. For instance,
in a case like the following:

diff --git a/xen/common/inflate.c b/xen/common/inflate.c
index 8fa4b96d12..8bdc9208da 100644
--- a/xen/common/inflate.c
+++ b/xen/common/inflate.c
@@ -1201,6 +1201,7 @@ static int __init gunzip(void)
     magic[1] = NEXTBYTE();
     method   = NEXTBYTE();
 
+    /* SAF-1-safe */
     if (magic[0] != 037 ||
         ((magic[1] != 0213) && (magic[1] != 0236))) {
         error("bad gzip magic numbers");


Would SAF-1-safe cover both 037, and also 0213 and 0213?
Or would it cover only 037?

We haven't use SAFE-n-safe extensively through the codebase yet but
my understanding is that SAFE-n-safe would cover the entire statement of
the following line, even if it is multi-line. Is that also your
understanding? Does it work like that with cppcheck?


It looks like ECLAIR requires a written-down number of lines of code to
deviate if it is more than 1 line. In this example it would be 2 lines:

     /* SAF-1-safe 2 */
     if (magic[0] != 037 ||
         ((magic[1] != 0213) && (magic[1] != 0236))) {

One option that I was thinking about is whether we can add the number of
lines automatically in xen-analysis based on the number of lines of the
next statement. What do you think?

It seems fragile to actually keep the number of lines inside the SAF
comment in the code. I am afraid it could get out of sync due to code
style refactoring or other mechanical changes.

Cheers,

Stefano

Re: xen-analysis ECLAIR support

[Nicola Vetrini]

On 25/08/2023 00:24, Stefano Stabellini wrote:
> Hi Luca,
> 
> We are looking into adding ECLAIR support for xen-analysis so that we
> can use the SAF-n-safe tags also with ECLAIR.
> 
> One question that came up is about multi-line statements. For instance,
> in a case like the following:
> 
> diff --git a/xen/common/inflate.c b/xen/common/inflate.c
> index 8fa4b96d12..8bdc9208da 100644
> --- a/xen/common/inflate.c
> +++ b/xen/common/inflate.c
> @@ -1201,6 +1201,7 @@ static int __init gunzip(void)
>      magic[1] = NEXTBYTE();
>      method   = NEXTBYTE();
> 
> +    /* SAF-1-safe */
>      if (magic[0] != 037 ||
>          ((magic[1] != 0213) && (magic[1] != 0236))) {
>          error("bad gzip magic numbers");
> 
> 
> Would SAF-1-safe cover both 037, and also 0213 and 0213?
> Or would it cover only 037?
> 
> We haven't use SAFE-n-safe extensively through the codebase yet but
> my understanding is that SAFE-n-safe would cover the entire statement 
> of
> the following line, even if it is multi-line. Is that also your
> understanding? Does it work like that with cppcheck?
> 
> 
> It looks like ECLAIR requires a written-down number of lines of code to
> deviate if it is more than 1 line. In this example it would be 2 lines:
> 
>      /* SAF-1-safe 2 */
>      if (magic[0] != 037 ||
>          ((magic[1] != 0213) && (magic[1] != 0236))) {
> 
> One option that I was thinking about is whether we can add the number 
> of
> lines automatically in xen-analysis based on the number of lines of the
> next statement. What do you think?
> 
> It seems fragile to actually keep the number of lines inside the SAF
> comment in the code. I am afraid it could get out of sync due to code
> style refactoring or other mechanical changes.
> 

Having the number of lines automatically inferred from the code 
following the comment
does not seem that robust either, given the minimal information in the 
SAF comments
(e.g., what if the whole if statement needs to be deviated, rather
than the controlling expression?).

An alternative proposal could be the following:
       /* SAF-n-safe begin */
       if (magic[0] != 037 ||
           ((magic[1] != 0213) && (magic[1] != 0236))) {
       /* SAF-n-safe end */

which is translated, for ECLAIR, into:

     /* -E> safe <Rule ID> 2 <free text> */
     if (magic[0] != 037 ||
           ((magic[1] != 0213) && (magic[1] != 0236))) {

this will deviate however many lines are between the begin and end 
markers.

-- 
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)

Re: xen-analysis ECLAIR support

[Michal Orzel]

Hi Stefano,

On 25/08/2023 00:24, Stefano Stabellini wrote:
> 
> 
> Hi Luca,
> 
> We are looking into adding ECLAIR support for xen-analysis so that we
> can use the SAF-n-safe tags also with ECLAIR.
> 
> One question that came up is about multi-line statements. For instance,
> in a case like the following:
> 
> diff --git a/xen/common/inflate.c b/xen/common/inflate.c
> index 8fa4b96d12..8bdc9208da 100644
> --- a/xen/common/inflate.c
> +++ b/xen/common/inflate.c
> @@ -1201,6 +1201,7 @@ static int __init gunzip(void)
>      magic[1] = NEXTBYTE();
>      method   = NEXTBYTE();
> 
> +    /* SAF-1-safe */
>      if (magic[0] != 037 ||
>          ((magic[1] != 0213) && (magic[1] != 0236))) {
>          error("bad gzip magic numbers");
> 
> 
> Would SAF-1-safe cover both 037, and also 0213 and 0213?
> Or would it cover only 037?
> 
> We haven't use SAFE-n-safe extensively through the codebase yet but
> my understanding is that SAFE-n-safe would cover the entire statement of
> the following line, even if it is multi-line. Is that also your
> understanding? Does it work like that with cppcheck?
Looking at the docs and the actual script, only the single line below SAF comment is excluded.
So in your case you would require:

/* SAF-1-safe */
if (magic[0] != 037 ||
    /* SAF-1-safe */
    ((magic[1] != 0213) && (magic[1] != 0236))) {
    error("bad gzip magic numbers");

I guess this was done so that it is clear that someone took all the parts of the statements into account
and all of them fall into the same justification (which might not be the case).

BTW. I don't think we have also covered the case where there is more than one violation in a single line
that we want to deviate (e.g. sth like /* SAF-1-safe, SAF-2-safe */

~Michal

Re: xen-analysis ECLAIR support

[Jan Beulich]

On 25.08.2023 10:18, Michal Orzel wrote:
> Hi Stefano,
> 
> On 25/08/2023 00:24, Stefano Stabellini wrote:
>>
>>
>> Hi Luca,
>>
>> We are looking into adding ECLAIR support for xen-analysis so that we
>> can use the SAF-n-safe tags also with ECLAIR.
>>
>> One question that came up is about multi-line statements. For instance,
>> in a case like the following:
>>
>> diff --git a/xen/common/inflate.c b/xen/common/inflate.c
>> index 8fa4b96d12..8bdc9208da 100644
>> --- a/xen/common/inflate.c
>> +++ b/xen/common/inflate.c
>> @@ -1201,6 +1201,7 @@ static int __init gunzip(void)
>>      magic[1] = NEXTBYTE();
>>      method   = NEXTBYTE();
>>
>> +    /* SAF-1-safe */
>>      if (magic[0] != 037 ||
>>          ((magic[1] != 0213) && (magic[1] != 0236))) {
>>          error("bad gzip magic numbers");
>>
>>
>> Would SAF-1-safe cover both 037, and also 0213 and 0213?
>> Or would it cover only 037?
>>
>> We haven't use SAFE-n-safe extensively through the codebase yet but
>> my understanding is that SAFE-n-safe would cover the entire statement of
>> the following line, even if it is multi-line. Is that also your
>> understanding? Does it work like that with cppcheck?
> Looking at the docs and the actual script, only the single line below SAF comment is excluded.
> So in your case you would require:
> 
> /* SAF-1-safe */
> if (magic[0] != 037 ||
>     /* SAF-1-safe */
>     ((magic[1] != 0213) && (magic[1] != 0236))) {
>     error("bad gzip magic numbers");

Or (perhaps more neatly):

    /* SAF-1-safe */
    if (magic[0] != 037 || (magic[1] != 0213 && magic[1] != 0236)) {
        error("bad gzip magic numbers");

Jan

Re: xen-analysis ECLAIR support

[Stefano Stabellini]

On Fri, 25 Aug 2023, Michal Orzel wrote:
> Hi Stefano,
> 
> On 25/08/2023 00:24, Stefano Stabellini wrote:
> > 
> > 
> > Hi Luca,
> > 
> > We are looking into adding ECLAIR support for xen-analysis so that we
> > can use the SAF-n-safe tags also with ECLAIR.
> > 
> > One question that came up is about multi-line statements. For instance,
> > in a case like the following:
> > 
> > diff --git a/xen/common/inflate.c b/xen/common/inflate.c
> > index 8fa4b96d12..8bdc9208da 100644
> > --- a/xen/common/inflate.c
> > +++ b/xen/common/inflate.c
> > @@ -1201,6 +1201,7 @@ static int __init gunzip(void)
> >      magic[1] = NEXTBYTE();
> >      method   = NEXTBYTE();
> > 
> > +    /* SAF-1-safe */
> >      if (magic[0] != 037 ||
> >          ((magic[1] != 0213) && (magic[1] != 0236))) {
> >          error("bad gzip magic numbers");
> > 
> > 
> > Would SAF-1-safe cover both 037, and also 0213 and 0213?
> > Or would it cover only 037?
> > 
> > We haven't use SAFE-n-safe extensively through the codebase yet but
> > my understanding is that SAFE-n-safe would cover the entire statement of
> > the following line, even if it is multi-line. Is that also your
> > understanding? Does it work like that with cppcheck?
> Looking at the docs and the actual script, only the single line below SAF comment is excluded.
> So in your case you would require:
> 
> /* SAF-1-safe */
> if (magic[0] != 037 ||
>     /* SAF-1-safe */
>     ((magic[1] != 0213) && (magic[1] != 0236))) {
>     error("bad gzip magic numbers");
> 
> I guess this was done so that it is clear that someone took all the parts of the statements into account
> and all of them fall into the same justification (which might not be the case).
 
Ops! In that case there is no difference between xen-analysis, cppcheck
and ECLAIR behaviors.


> BTW. I don't think we have also covered the case where there is more than one violation in a single line
> that we want to deviate (e.g. sth like /* SAF-1-safe, SAF-2-safe */

Good point. Yes we need to make sure that case is covered as well
one way or the other.

Re: xen-analysis ECLAIR support

[Stefano Stabellini]

On Fri, 25 Aug 2023, Nicola Vetrini wrote:
> On 25/08/2023 00:24, Stefano Stabellini wrote:
> > Hi Luca,
> > 
> > We are looking into adding ECLAIR support for xen-analysis so that we
> > can use the SAF-n-safe tags also with ECLAIR.
> > 
> > One question that came up is about multi-line statements. For instance,
> > in a case like the following:
> > 
> > diff --git a/xen/common/inflate.c b/xen/common/inflate.c
> > index 8fa4b96d12..8bdc9208da 100644
> > --- a/xen/common/inflate.c
> > +++ b/xen/common/inflate.c
> > @@ -1201,6 +1201,7 @@ static int __init gunzip(void)
> >      magic[1] = NEXTBYTE();
> >      method   = NEXTBYTE();
> > 
> > +    /* SAF-1-safe */
> >      if (magic[0] != 037 ||
> >          ((magic[1] != 0213) && (magic[1] != 0236))) {
> >          error("bad gzip magic numbers");
> > 
> > 
> > Would SAF-1-safe cover both 037, and also 0213 and 0213?
> > Or would it cover only 037?
> > 
> > We haven't use SAFE-n-safe extensively through the codebase yet but
> > my understanding is that SAFE-n-safe would cover the entire statement of
> > the following line, even if it is multi-line. Is that also your
> > understanding? Does it work like that with cppcheck?
> > 
> > 
> > It looks like ECLAIR requires a written-down number of lines of code to
> > deviate if it is more than 1 line. In this example it would be 2 lines:
> > 
> >      /* SAF-1-safe 2 */
> >      if (magic[0] != 037 ||
> >          ((magic[1] != 0213) && (magic[1] != 0236))) {
> > 
> > One option that I was thinking about is whether we can add the number of
> > lines automatically in xen-analysis based on the number of lines of the
> > next statement. What do you think?
> > 
> > It seems fragile to actually keep the number of lines inside the SAF
> > comment in the code. I am afraid it could get out of sync due to code
> > style refactoring or other mechanical changes.
> > 
> 
> Having the number of lines automatically inferred from the code following the
> comment
> does not seem that robust either, given the minimal information in the SAF
> comments
> (e.g., what if the whole if statement needs to be deviated, rather
> than the controlling expression?).
> 
> An alternative proposal could be the following:
>       /* SAF-n-safe begin */
>       if (magic[0] != 037 ||
>           ((magic[1] != 0213) && (magic[1] != 0236))) {
>       /* SAF-n-safe end */
> 
> which is translated, for ECLAIR, into:
> 
>     /* -E> safe <Rule ID> 2 <free text> */
>     if (magic[0] != 037 ||
>           ((magic[1] != 0213) && (magic[1] != 0236))) {
> 
> this will deviate however many lines are between the begin and end markers.

I think this could be a good way to solve the problem when multi-line
deviation support is required. In this case, like Jan suggested, it
is easier to put everything on a single line, but in other cases it
might not be possible.

Re: xen-analysis ECLAIR support

[Luca Fancellu]

> On 25 Aug 2023, at 09:18, Michal Orzel <michal.orzel@amd.com> wrote:
> 
> Hi Stefano,
> 
> On 25/08/2023 00:24, Stefano Stabellini wrote:
>> 
>> 
>> Hi Luca,
>> 
>> We are looking into adding ECLAIR support for xen-analysis so that we
>> can use the SAF-n-safe tags also with ECLAIR.
>> 
>> One question that came up is about multi-line statements. For instance,
>> in a case like the following:
>> 
>> diff --git a/xen/common/inflate.c b/xen/common/inflate.c
>> index 8fa4b96d12..8bdc9208da 100644
>> --- a/xen/common/inflate.c
>> +++ b/xen/common/inflate.c
>> @@ -1201,6 +1201,7 @@ static int __init gunzip(void)
>>     magic[1] = NEXTBYTE();
>>     method   = NEXTBYTE();
>> 
>> +    /* SAF-1-safe */
>>     if (magic[0] != 037 ||
>>         ((magic[1] != 0213) && (magic[1] != 0236))) {
>>         error("bad gzip magic numbers");
>> 
>> 
>> Would SAF-1-safe cover both 037, and also 0213 and 0213?
>> Or would it cover only 037?
>> 
>> We haven't use SAFE-n-safe extensively through the codebase yet but
>> my understanding is that SAFE-n-safe would cover the entire statement of
>> the following line, even if it is multi-line. Is that also your
>> understanding? Does it work like that with cppcheck?
> Looking at the docs and the actual script, only the single line below SAF comment is excluded.
> So in your case you would require:
> 
> /* SAF-1-safe */
> if (magic[0] != 037 ||
>    /* SAF-1-safe */
>    ((magic[1] != 0213) && (magic[1] != 0236))) {
>    error("bad gzip magic numbers");

Yes correct

> 
> I guess this was done so that it is clear that someone took all the parts of the statements into account
> and all of them fall into the same justification (which might not be the case).
> 
> BTW. I don't think we have also covered the case where there is more than one violation in a single line
> that we want to deviate (e.g. sth like /* SAF-1-safe, SAF-2-safe */

You are right, but it should work adding multiple comments in this way:

/* SAF-1-safe */
/* SAF-2-safe */
<code where violation 1 and 2 are in the same line>

> 
> ~Michal

Re: xen-analysis ECLAIR support

[Luca Fancellu]

> On 25 Aug 2023, at 09:28, Jan Beulich <jbeulich@suse.com> wrote:
> 
> On 25.08.2023 10:18, Michal Orzel wrote:
>> Hi Stefano,
>> 
>> On 25/08/2023 00:24, Stefano Stabellini wrote:
>>> 
>>> 
>>> Hi Luca,
>>> 
>>> We are looking into adding ECLAIR support for xen-analysis so that we
>>> can use the SAF-n-safe tags also with ECLAIR.
>>> 
>>> One question that came up is about multi-line statements. For instance,
>>> in a case like the following:
>>> 
>>> diff --git a/xen/common/inflate.c b/xen/common/inflate.c
>>> index 8fa4b96d12..8bdc9208da 100644
>>> --- a/xen/common/inflate.c
>>> +++ b/xen/common/inflate.c
>>> @@ -1201,6 +1201,7 @@ static int __init gunzip(void)
>>>     magic[1] = NEXTBYTE();
>>>     method   = NEXTBYTE();
>>> 
>>> +    /* SAF-1-safe */
>>>     if (magic[0] != 037 ||
>>>         ((magic[1] != 0213) && (magic[1] != 0236))) {
>>>         error("bad gzip magic numbers");
>>> 
>>> 
>>> Would SAF-1-safe cover both 037, and also 0213 and 0213?
>>> Or would it cover only 037?
>>> 
>>> We haven't use SAFE-n-safe extensively through the codebase yet but
>>> my understanding is that SAFE-n-safe would cover the entire statement of
>>> the following line, even if it is multi-line. Is that also your
>>> understanding? Does it work like that with cppcheck?
>> Looking at the docs and the actual script, only the single line below SAF comment is excluded.
>> So in your case you would require:
>> 
>> /* SAF-1-safe */
>> if (magic[0] != 037 ||
>>    /* SAF-1-safe */
>>    ((magic[1] != 0213) && (magic[1] != 0236))) {
>>    error("bad gzip magic numbers");
> 
> Or (perhaps more neatly):
> 
>    /* SAF-1-safe */
>    if (magic[0] != 037 || (magic[1] != 0213 && magic[1] != 0236)) {
>        error("bad gzip magic numbers");

+1 for this approach, I was going to suggest it

> 
> Jan

Re: xen-analysis ECLAIR support

[Luca Fancellu]

> On 25 Aug 2023, at 22:56, Stefano Stabellini <sstabellini@kernel.org> wrote:
> 
> On Fri, 25 Aug 2023, Nicola Vetrini wrote:
>> On 25/08/2023 00:24, Stefano Stabellini wrote:
>>> Hi Luca,
>>> 
>>> We are looking into adding ECLAIR support for xen-analysis so that we
>>> can use the SAF-n-safe tags also with ECLAIR.
>>> 
>>> One question that came up is about multi-line statements. For instance,
>>> in a case like the following:
>>> 
>>> diff --git a/xen/common/inflate.c b/xen/common/inflate.c
>>> index 8fa4b96d12..8bdc9208da 100644
>>> --- a/xen/common/inflate.c
>>> +++ b/xen/common/inflate.c
>>> @@ -1201,6 +1201,7 @@ static int __init gunzip(void)
>>>     magic[1] = NEXTBYTE();
>>>     method   = NEXTBYTE();
>>> 
>>> +    /* SAF-1-safe */
>>>     if (magic[0] != 037 ||
>>>         ((magic[1] != 0213) && (magic[1] != 0236))) {
>>>         error("bad gzip magic numbers");
>>> 
>>> 
>>> Would SAF-1-safe cover both 037, and also 0213 and 0213?
>>> Or would it cover only 037?
>>> 
>>> We haven't use SAFE-n-safe extensively through the codebase yet but
>>> my understanding is that SAFE-n-safe would cover the entire statement of
>>> the following line, even if it is multi-line. Is that also your
>>> understanding? Does it work like that with cppcheck?
>>> 
>>> 
>>> It looks like ECLAIR requires a written-down number of lines of code to
>>> deviate if it is more than 1 line. In this example it would be 2 lines:
>>> 
>>>     /* SAF-1-safe 2 */
>>>     if (magic[0] != 037 ||
>>>         ((magic[1] != 0213) && (magic[1] != 0236))) {
>>> 
>>> One option that I was thinking about is whether we can add the number of
>>> lines automatically in xen-analysis based on the number of lines of the
>>> next statement. What do you think?
>>> 
>>> It seems fragile to actually keep the number of lines inside the SAF
>>> comment in the code. I am afraid it could get out of sync due to code
>>> style refactoring or other mechanical changes.
>>> 
>> 
>> Having the number of lines automatically inferred from the code following the
>> comment
>> does not seem that robust either, given the minimal information in the SAF
>> comments
>> (e.g., what if the whole if statement needs to be deviated, rather
>> than the controlling expression?).
>> 
>> An alternative proposal could be the following:
>>      /* SAF-n-safe begin */
>>      if (magic[0] != 037 ||
>>          ((magic[1] != 0213) && (magic[1] != 0236))) {
>>      /* SAF-n-safe end */
>> 
>> which is translated, for ECLAIR, into:
>> 
>>    /* -E> safe <Rule ID> 2 <free text> */
>>    if (magic[0] != 037 ||
>>          ((magic[1] != 0213) && (magic[1] != 0236))) {
>> 
>> this will deviate however many lines are between the begin and end markers.
> 
> I think this could be a good way to solve the problem when multi-line
> deviation support is required. In this case, like Jan suggested, it
> is easier to put everything on a single line, but in other cases it
> might not be possible.

Yes, in that case however we are tied to what the underlying tool are supporting,
for example eclair is pretty nice and support an in-code comment with advanced
Syntax, but for example cppcheck and also coverity don’t, so in the end we used
the common denominator where the comment suppress the next line (containing code).