Re: xen-analysis ECLAIR support

[Stefano Stabellini <sstabellini@xxxxxxxxxx>]

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.