[XEN PATCH v4 0/2] use the documentation for MISRA C:2012 Dir 4.1

[XEN PATCH v4 0/2] use the documentation for MISRA C:2012 Dir 4.1

[Nicola Vetrini]

This series addresses some concerns raised on patches 2 and 3 from [1].
Note that patch 1 from that series has already been applied.

Patch 1 comprises a modified version of patches 2 and 3 of the previous series.
Patch 2 is brand new, as it merely clarifies how to write such documentation.

[1] https://lore.kernel.org/xen-devel/cover.1696231870.git.nicola.vetrini@bugseng.com/

Nicola Vetrini (2):
  automation/eclair: make the docs for MISRA C:2012 Dir 4.1 visible to
    ECLAIR
  docs/misra: add guidance on the format of  Dir 4.1 docs for ECLAIR

 automation/eclair_analysis/build.sh   | 21 +++++++++++++++++++--
 automation/eclair_analysis/prepare.sh |  7 ++++---
 docs/misra/C-runtime-failures.rst     |  8 ++++++++
 3 files changed, 31 insertions(+), 5 deletions(-)

-- 
2.34.1

[XEN PATCH v4 1/2] automation/eclair: make the docs for MISRA C:2012 Dir 4.1 visible to ECLAIR

[Nicola Vetrini]

To be able to check for the existence of the necessary subsections in
the documentation for MISRA C:2012 Dir 4.1, ECLAIR needs to have a source
file that is built.

This file is generated from 'C-runtime-failures.rst' in docs/misra
and the configuration is updated accordingly.

Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
---
Changes from RFC:
- Dropped unused/useless code
- Revised the sed command
- Revised the clean target

Changes in v2:
- Added explanative comment to the makefile
- printf instead of echo

Changes in v3:
- Terminate the generated file with a newline
- Build it with -std=c99, so that the documentation
  for D1.1 applies.
Changes in v5:
- Transform and build the file directly in the eclair-specific directory
---
 automation/eclair_analysis/build.sh   | 21 +++++++++++++++++++--
 automation/eclair_analysis/prepare.sh |  7 ++++---
 2 files changed, 23 insertions(+), 5 deletions(-)

diff --git a/automation/eclair_analysis/build.sh b/automation/eclair_analysis/build.sh
index ec087dd822fa..f24292ed0643 100755
--- a/automation/eclair_analysis/build.sh
+++ b/automation/eclair_analysis/build.sh
@@ -33,12 +33,29 @@ else
   PROCESSORS=6
 fi
 
+runtime_failures_docs() {
+  doc="C-runtime-failures.rst"
+  builddir="automation/eclair_analysis"
+  
+  cp "docs/misra/${doc}" "${builddir}"
+  cd "${builddir}"
+  printf "/*\n\n" >"${doc}.tmp"
+  sed -e 's|\*/|*//*|g' "${doc}" >>"${doc}.tmp"
+  printf "\n\n*/\n" >>"${doc}.tmp"
+  mv "${doc}.tmp" "${doc}.c"
+  
+  # Cannot redirect to /dev/null because it would be excluded from the analysis
+  "${CROSS_COMPILE}gcc-12" -std=c99 -c "${doc}.c" -o "${doc}.o"
+  cd -
+}
+
 (
-  cd xen
+  runtime_failures_docs
 
   make "-j${PROCESSORS}" "-l${PROCESSORS}.0"    \
        "CROSS_COMPILE=${CROSS_COMPILE}"         \
        "CC=${CROSS_COMPILE}gcc-12"              \
        "CXX=${CROSS_COMPILE}g++-12"             \
-       "XEN_TARGET_ARCH=${XEN_TARGET_ARCH}"
+       "XEN_TARGET_ARCH=${XEN_TARGET_ARCH}"     \
+       -C xen
 )
diff --git a/automation/eclair_analysis/prepare.sh b/automation/eclair_analysis/prepare.sh
index 0cac5eba00ae..fe9d16e48ecc 100755
--- a/automation/eclair_analysis/prepare.sh
+++ b/automation/eclair_analysis/prepare.sh
@@ -35,11 +35,12 @@ else
 fi
 
 (
-    cd xen
-    cp "${CONFIG_FILE}" .config
+    ./configure
+    cp "${CONFIG_FILE}" xen/.config
     make clean
     find . -type f -name "*.safparse" -print -delete
-    make -f ${script_dir}/Makefile.prepare prepare
+    cd xen
+    make -f "${script_dir}/Makefile.prepare" prepare
     # Translate the /* SAF-n-safe */ comments into ECLAIR CBTs
     scripts/xen-analysis.py --run-eclair --no-build --no-clean
 )
-- 
2.34.1

Re: [XEN PATCH v4 1/2] automation/eclair: make the docs for MISRA C:2012 Dir 4.1 visible to ECLAIR

[Stefano Stabellini]

On Tue, 14 Nov 2023, Nicola Vetrini wrote:
> To be able to check for the existence of the necessary subsections in
> the documentation for MISRA C:2012 Dir 4.1, ECLAIR needs to have a source
> file that is built.
> 
> This file is generated from 'C-runtime-failures.rst' in docs/misra
> and the configuration is updated accordingly.
> 
> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>

This is actually match better than before, thanks!

Reviewed-by: Stefano Stabellini <sstabellini@kernel.org>

Re: [XEN PATCH v4 1/2] automation/eclair: make the docs for MISRA C:2012 Dir 4.1 visible to ECLAIR

[Julien Grall]

Hi,

On 14/11/2023 15:36, Nicola Vetrini wrote:
> To be able to check for the existence of the necessary subsections in
> the documentation for MISRA C:2012 Dir 4.1, ECLAIR needs to have a source
> file that is built.
> 
> This file is generated from 'C-runtime-failures.rst' in docs/misra
> and the configuration is updated accordingly.
> 
> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
> ---
> Changes from RFC:
> - Dropped unused/useless code
> - Revised the sed command
> - Revised the clean target
> 
> Changes in v2:
> - Added explanative comment to the makefile
> - printf instead of echo
> 
> Changes in v3:
> - Terminate the generated file with a newline
> - Build it with -std=c99, so that the documentation
>    for D1.1 applies.
> Changes in v5:
> - Transform and build the file directly in the eclair-specific directory
> ---
>   automation/eclair_analysis/build.sh   | 21 +++++++++++++++++++--
>   automation/eclair_analysis/prepare.sh |  7 ++++---
>   2 files changed, 23 insertions(+), 5 deletions(-)
> 
> diff --git a/automation/eclair_analysis/build.sh b/automation/eclair_analysis/build.sh
> index ec087dd822fa..f24292ed0643 100755
> --- a/automation/eclair_analysis/build.sh
> +++ b/automation/eclair_analysis/build.sh
> @@ -33,12 +33,29 @@ else
>     PROCESSORS=6
>   fi
>   
> +runtime_failures_docs() {
> +  doc="C-runtime-failures.rst"
> +  builddir="automation/eclair_analysis"
> +
> +  cp "docs/misra/${doc}" "${builddir}"

Is it necessary to copy the .rst? IOW, would it be sufficient to use...

> +  cd "${builddir}"
> +  printf "/*\n\n" >"${doc}.tmp"
> +  sed -e 's|\*/|*//*|g' "${doc}" >>"${doc}.tmp"

... docs/misc/${doc} here?

> +  printf "\n\n*/\n" >>"${doc}.tmp"
> +  mv "${doc}.tmp" "${doc}.c"

NIT: I am not sure why you need to first create .tmp and then create.c.

> +
> +  # Cannot redirect to /dev/null because it would be excluded from the analysis
> +  "${CROSS_COMPILE}gcc-12" -std=c99 -c "${doc}.c" -o "${doc}.o"

NIT: It would be helpful to specify why -std=c99 is used. Above, you 
suggest this is to enable D1.1.

NIT: Can we define CC and use here and ...

> +  cd -
> +}
> +
>   (
> -  cd xen
> +  runtime_failures_docs
>   
>     make "-j${PROCESSORS}" "-l${PROCESSORS}.0"    \
>          "CROSS_COMPILE=${CROSS_COMPILE}"         \
>          "CC=${CROSS_COMPILE}gcc-12"              \

...? This would make easier to re-use the code.

>          "CXX=${CROSS_COMPILE}g++-12"             \
> -       "XEN_TARGET_ARCH=${XEN_TARGET_ARCH}"
> +       "XEN_TARGET_ARCH=${XEN_TARGET_ARCH}"     \
> +       -C xen
>   )
> diff --git a/automation/eclair_analysis/prepare.sh b/automation/eclair_analysis/prepare.sh
> index 0cac5eba00ae..fe9d16e48ecc 100755
> --- a/automation/eclair_analysis/prepare.sh
> +++ b/automation/eclair_analysis/prepare.sh
> @@ -35,11 +35,12 @@ else
>   fi
>   
>   (
> -    cd xen
> -    cp "${CONFIG_FILE}" .config
> +    ./configure
> +    cp "${CONFIG_FILE}" xen/.config
>       make clean
>       find . -type f -name "*.safparse" -print -delete
> -    make -f ${script_dir}/Makefile.prepare prepare
> +    cd xen
> +    make -f "${script_dir}/Makefile.prepare" prepare
>       # Translate the /* SAF-n-safe */ comments into ECLAIR CBTs
>       scripts/xen-analysis.py --run-eclair --no-build --no-clean
>   )

Cheers,

-- 
Julien Grall

Re: [XEN PATCH v4 1/2] automation/eclair: make the docs for MISRA C:2012 Dir 4.1 visible to ECLAIR

[Nicola Vetrini]

On 2023-11-14 23:12, Julien Grall wrote:
> Hi,
> 
> On 14/11/2023 15:36, Nicola Vetrini wrote:
>> To be able to check for the existence of the necessary subsections in
>> the documentation for MISRA C:2012 Dir 4.1, ECLAIR needs to have a 
>> source
>> file that is built.
>> 
>> This file is generated from 'C-runtime-failures.rst' in docs/misra
>> and the configuration is updated accordingly.
>> 
>> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
>> ---
>> Changes from RFC:
>> - Dropped unused/useless code
>> - Revised the sed command
>> - Revised the clean target
>> 
>> Changes in v2:
>> - Added explanative comment to the makefile
>> - printf instead of echo
>> 
>> Changes in v3:
>> - Terminate the generated file with a newline
>> - Build it with -std=c99, so that the documentation
>>    for D1.1 applies.
>> Changes in v5:
>> - Transform and build the file directly in the eclair-specific 
>> directory
>> ---
>>   automation/eclair_analysis/build.sh   | 21 +++++++++++++++++++--
>>   automation/eclair_analysis/prepare.sh |  7 ++++---
>>   2 files changed, 23 insertions(+), 5 deletions(-)
>> 
>> diff --git a/automation/eclair_analysis/build.sh 
>> b/automation/eclair_analysis/build.sh
>> index ec087dd822fa..f24292ed0643 100755
>> --- a/automation/eclair_analysis/build.sh
>> +++ b/automation/eclair_analysis/build.sh
>> @@ -33,12 +33,29 @@ else
>>     PROCESSORS=6
>>   fi
>>   +runtime_failures_docs() {
>> +  doc="C-runtime-failures.rst"
>> +  builddir="automation/eclair_analysis"
>> +
>> +  cp "docs/misra/${doc}" "${builddir}"
> 
> Is it necessary to copy the .rst? IOW, would it be sufficient to use...
> 
>> +  cd "${builddir}"
>> +  printf "/*\n\n" >"${doc}.tmp"
>> +  sed -e 's|\*/|*//*|g' "${doc}" >>"${doc}.tmp"
> 
> ... docs/misc/${doc} here?
> 

I didn't want to leave a stray file under docs/misra, but it's not 
essential.

>> +  printf "\n\n*/\n" >>"${doc}.tmp"
>> +  mv "${doc}.tmp" "${doc}.c"
> 
> NIT: I am not sure why you need to first create .tmp and then create.c.
> 

Wasn't this a pattern to defend against interruptions of the build, just 
as I did in v3?

+$(TARGETS:.o=.c): %.c: %.rst
+    printf "/*\n\n" > $@.tmp
+    sed -e 's|\*/|*//*|g' $< >> $@.tmp
+    printf "\n\n*/\n" >> $@.tmp
+    mv $@.tmp $@

>> +
>> +  # Cannot redirect to /dev/null because it would be excluded from 
>> the analysis
>> +  "${CROSS_COMPILE}gcc-12" -std=c99 -c "${doc}.c" -o "${doc}.o"
> 
> NIT: It would be helpful to specify why -std=c99 is used. Above, you 
> suggest this is to enable D1.1.
> 

Yeah, the comment in the changelog should be pasted here

> NIT: Can we define CC and use here and ...
> 
>> +  cd -
>> +}
>> +
>>   (
>> -  cd xen
>> +  runtime_failures_docs
>>       make "-j${PROCESSORS}" "-l${PROCESSORS}.0"    \
>>          "CROSS_COMPILE=${CROSS_COMPILE}"         \
>>          "CC=${CROSS_COMPILE}gcc-12"              \
> 
> ...? This would make easier to re-use the code.
> 

I don't expect this build script to be changed much to be honest, but if 
you think
this is beneficial then it's ok.

>>          "CXX=${CROSS_COMPILE}g++-12"             \
>> -       "XEN_TARGET_ARCH=${XEN_TARGET_ARCH}"
>> +       "XEN_TARGET_ARCH=${XEN_TARGET_ARCH}"     \
>> +       -C xen
>>   )
>> diff --git a/automation/eclair_analysis/prepare.sh 
>> b/automation/eclair_analysis/prepare.sh
>> index 0cac5eba00ae..fe9d16e48ecc 100755
>> --- a/automation/eclair_analysis/prepare.sh
>> +++ b/automation/eclair_analysis/prepare.sh
>> @@ -35,11 +35,12 @@ else
>>   fi
>>     (
>> -    cd xen
>> -    cp "${CONFIG_FILE}" .config
>> +    ./configure
>> +    cp "${CONFIG_FILE}" xen/.config
>>       make clean
>>       find . -type f -name "*.safparse" -print -delete
>> -    make -f ${script_dir}/Makefile.prepare prepare
>> +    cd xen
>> +    make -f "${script_dir}/Makefile.prepare" prepare
>>       # Translate the /* SAF-n-safe */ comments into ECLAIR CBTs
>>       scripts/xen-analysis.py --run-eclair --no-build --no-clean
>>   )
> 
> Cheers,

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

Re: [XEN PATCH v4 1/2] automation/eclair: make the docs for MISRA C:2012 Dir 4.1 visible to ECLAIR

[Julien Grall]

Hi,

On 15/11/2023 11:02, Nicola Vetrini wrote:
> On 2023-11-14 23:12, Julien Grall wrote:
>> Hi,
>>
>> On 14/11/2023 15:36, Nicola Vetrini wrote:
>>> To be able to check for the existence of the necessary subsections in
>>> the documentation for MISRA C:2012 Dir 4.1, ECLAIR needs to have a 
>>> source
>>> file that is built.
>>>
>>> This file is generated from 'C-runtime-failures.rst' in docs/misra
>>> and the configuration is updated accordingly.
>>>
>>> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
>>> ---
>>> Changes from RFC:
>>> - Dropped unused/useless code
>>> - Revised the sed command
>>> - Revised the clean target
>>>
>>> Changes in v2:
>>> - Added explanative comment to the makefile
>>> - printf instead of echo
>>>
>>> Changes in v3:
>>> - Terminate the generated file with a newline
>>> - Build it with -std=c99, so that the documentation
>>>    for D1.1 applies.
>>> Changes in v5:
>>> - Transform and build the file directly in the eclair-specific directory
>>> ---
>>>   automation/eclair_analysis/build.sh   | 21 +++++++++++++++++++--
>>>   automation/eclair_analysis/prepare.sh |  7 ++++---
>>>   2 files changed, 23 insertions(+), 5 deletions(-)
>>>
>>> diff --git a/automation/eclair_analysis/build.sh 
>>> b/automation/eclair_analysis/build.sh
>>> index ec087dd822fa..f24292ed0643 100755
>>> --- a/automation/eclair_analysis/build.sh
>>> +++ b/automation/eclair_analysis/build.sh
>>> @@ -33,12 +33,29 @@ else
>>>     PROCESSORS=6
>>>   fi
>>>   +runtime_failures_docs() {
>>> +  doc="C-runtime-failures.rst"
>>> +  builddir="automation/eclair_analysis"
>>> +
>>> +  cp "docs/misra/${doc}" "${builddir}"
>>
>> Is it necessary to copy the .rst? IOW, would it be sufficient to use...
>>
>>> +  cd "${builddir}"
>>> +  printf "/*\n\n" >"${doc}.tmp"
>>> +  sed -e 's|\*/|*//*|g' "${doc}" >>"${doc}.tmp"
>>
>> ... docs/misc/${doc} here?
>>
> 
> I didn't want to leave a stray file under docs/misra, but it's not 
> essential.

I am confused. I am suggesting to use:

sed -e 's|\*/|*//*|g' "../../docs/misc/${doc}" >> "${doc}.tmp"

So *.tmp is still created at the same place.

> 
>>> +  printf "\n\n*/\n" >>"${doc}.tmp"
>>> +  mv "${doc}.tmp" "${doc}.c"
>>
>> NIT: I am not sure why you need to first create .tmp and then create.c.
>>
> 
> Wasn't this a pattern to defend against interruptions of the build, just 
> as I did in v3?
> 
> +$(TARGETS:.o=.c): %.c: %.rst
> +    printf "/*\n\n" > $@.tmp
> +    sed -e 's|\*/|*//*|g' $< >> $@.tmp
> +    printf "\n\n*/\n" >> $@.tmp
> +    mv $@.tmp $@

Yes but it makes sense for the Makefile because the target would not be 
re-executed if *.c exists.

But I don't think this is the case for you because you are using a bash 
script. So your function should always be re-executed regardless on 
whether it was interrupted or not.

> 
>>> +
>>> +  # Cannot redirect to /dev/null because it would be excluded from 
>>> the analysis
>>> +  "${CROSS_COMPILE}gcc-12" -std=c99 -c "${doc}.c" -o "${doc}.o"
>>
>> NIT: It would be helpful to specify why -std=c99 is used. Above, you 
>> suggest this is to enable D1.1.
>>
> 
> Yeah, the comment in the changelog should be pasted here
> 
>> NIT: Can we define CC and use here and ...
>>
>>> +  cd -
>>> +}
>>> +
>>>   (
>>> -  cd xen
>>> +  runtime_failures_docs
>>>       make "-j${PROCESSORS}" "-l${PROCESSORS}.0"    \
>>>          "CROSS_COMPILE=${CROSS_COMPILE}"         \
>>>          "CC=${CROSS_COMPILE}gcc-12"              \
>>
>> ...? This would make easier to re-use the code.
>>
> 
> I don't expect this build script to be changed much to be honest, but if 
> you think
> this is beneficial then it's ok.

This is not only about code evolving. It makes easier to spot your are 
using the same compiler. I would not have made the remark if you were 
using 'gcc'.

But I noticed you were using gcc-12 and originally thought it was a 
mistake until I saw the second use.

The advantage of a variable CC (and CXX) is you can add a comment on top 
why you are specifically requestion gcc-12? IOW, why is gcc not fine?

Cheers,

-- 
Julien Grall

Re: [XEN PATCH v4 1/2] automation/eclair: make the docs for MISRA C:2012 Dir 4.1 visible to ECLAIR

[Nicola Vetrini]

On 2023-11-15 12:22, Julien Grall wrote:
> Hi,
> 
> On 15/11/2023 11:02, Nicola Vetrini wrote:
>> On 2023-11-14 23:12, Julien Grall wrote:
>>> Hi,
>>> 
>>> On 14/11/2023 15:36, Nicola Vetrini wrote:
>>>> To be able to check for the existence of the necessary subsections 
>>>> in
>>>> the documentation for MISRA C:2012 Dir 4.1, ECLAIR needs to have a 
>>>> source
>>>> file that is built.
>>>> 
>>>> This file is generated from 'C-runtime-failures.rst' in docs/misra
>>>> and the configuration is updated accordingly.
>>>> 
>>>> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
>>>> ---
>>>> Changes from RFC:
>>>> - Dropped unused/useless code
>>>> - Revised the sed command
>>>> - Revised the clean target
>>>> 
>>>> Changes in v2:
>>>> - Added explanative comment to the makefile
>>>> - printf instead of echo
>>>> 
>>>> Changes in v3:
>>>> - Terminate the generated file with a newline
>>>> - Build it with -std=c99, so that the documentation
>>>>    for D1.1 applies.
>>>> Changes in v5:
>>>> - Transform and build the file directly in the eclair-specific 
>>>> directory
>>>> ---
>>>>   automation/eclair_analysis/build.sh   | 21 +++++++++++++++++++--
>>>>   automation/eclair_analysis/prepare.sh |  7 ++++---
>>>>   2 files changed, 23 insertions(+), 5 deletions(-)
>>>> 
>>>> diff --git a/automation/eclair_analysis/build.sh 
>>>> b/automation/eclair_analysis/build.sh
>>>> index ec087dd822fa..f24292ed0643 100755
>>>> --- a/automation/eclair_analysis/build.sh
>>>> +++ b/automation/eclair_analysis/build.sh
>>>> @@ -33,12 +33,29 @@ else
>>>>     PROCESSORS=6
>>>>   fi
>>>>   +runtime_failures_docs() {
>>>> +  doc="C-runtime-failures.rst"
>>>> +  builddir="automation/eclair_analysis"
>>>> +
>>>> +  cp "docs/misra/${doc}" "${builddir}"
>>> 
>>> Is it necessary to copy the .rst? IOW, would it be sufficient to 
>>> use...
>>> 
>>>> +  cd "${builddir}"
>>>> +  printf "/*\n\n" >"${doc}.tmp"
>>>> +  sed -e 's|\*/|*//*|g' "${doc}" >>"${doc}.tmp"
>>> 
>>> ... docs/misc/${doc} here?
>>> 
>> 
>> I didn't want to leave a stray file under docs/misra, but it's not 
>> essential.
> 
> I am confused. I am suggesting to use:
> 
> sed -e 's|\*/|*//*|g' "../../docs/misc/${doc}" >> "${doc}.tmp"
> 
> So *.tmp is still created at the same place.
> 

Ok, makes sense.

>> 
>>>> +  printf "\n\n*/\n" >>"${doc}.tmp"
>>>> +  mv "${doc}.tmp" "${doc}.c"
>>> 
>>> NIT: I am not sure why you need to first create .tmp and then 
>>> create.c.
>>> 
>> 
>> Wasn't this a pattern to defend against interruptions of the build, 
>> just as I did in v3?
>> 
>> +$(TARGETS:.o=.c): %.c: %.rst
>> +    printf "/*\n\n" > $@.tmp
>> +    sed -e 's|\*/|*//*|g' $< >> $@.tmp
>> +    printf "\n\n*/\n" >> $@.tmp
>> +    mv $@.tmp $@
> 
> Yes but it makes sense for the Makefile because the target would not be 
> re-executed if *.c exists.
> 
> But I don't think this is the case for you because you are using a bash 
> script. So your function should always be re-executed regardless on 
> whether it was interrupted or not.
> 

Ok.

>> 
>>>> +
>>>> +  # Cannot redirect to /dev/null because it would be excluded from 
>>>> the analysis
>>>> +  "${CROSS_COMPILE}gcc-12" -std=c99 -c "${doc}.c" -o "${doc}.o"
>>> 
>>> NIT: It would be helpful to specify why -std=c99 is used. Above, you 
>>> suggest this is to enable D1.1.
>>> 
>> 
>> Yeah, the comment in the changelog should be pasted here
>> 
>>> NIT: Can we define CC and use here and ...
>>> 
>>>> +  cd -
>>>> +}
>>>> +
>>>>   (
>>>> -  cd xen
>>>> +  runtime_failures_docs
>>>>       make "-j${PROCESSORS}" "-l${PROCESSORS}.0"    \
>>>>          "CROSS_COMPILE=${CROSS_COMPILE}"         \
>>>>          "CC=${CROSS_COMPILE}gcc-12"              \
>>> 
>>> ...? This would make easier to re-use the code.
>>> 
>> 
>> I don't expect this build script to be changed much to be honest, but 
>> if you think
>> this is beneficial then it's ok.
> 
> This is not only about code evolving. It makes easier to spot your are 
> using the same compiler. I would not have made the remark if you were 
> using 'gcc'.
> 
> But I noticed you were using gcc-12 and originally thought it was a 
> mistake until I saw the second use.
> 
> The advantage of a variable CC (and CXX) is you can add a comment on 
> top why you are specifically requestion gcc-12? IOW, why is gcc not 
> fine?
> 

The assumptions in C-language-toolchain.rst (which are reflected in the 
analysis config) are using gcc-12 explicitly; that's just easier from a 
certification perspective to have a fixed version.

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

Re: [XEN PATCH v4 1/2] automation/eclair: make the docs for MISRA C:2012 Dir 4.1 visible to ECLAIR

[Jan Beulich]

On 16.11.2023 09:45, Nicola Vetrini wrote:
> On 2023-11-15 12:22, Julien Grall wrote:
>> But I noticed you were using gcc-12 and originally thought it was a 
>> mistake until I saw the second use.
>>
>> The advantage of a variable CC (and CXX) is you can add a comment on 
>> top why you are specifically requestion gcc-12? IOW, why is gcc not 
>> fine?
>>
> 
> The assumptions in C-language-toolchain.rst (which are reflected in the 
> analysis config) are using gcc-12 explicitly; that's just easier from a 
> certification perspective to have a fixed version.

I'm wondering: Upstream Xen isn't going to undergo any certification
effort, aiui. Downstreams who want to do so may have good reasons to
choose a specific compiler version, which may well not be gcc12. How
are we meaning to deal with that?

Jan

Re: [XEN PATCH v4 1/2] automation/eclair: make the docs for MISRA C:2012 Dir 4.1 visible to ECLAIR

[Stefano Stabellini]

On Thu, 16 Nov 2023, Jan Beulich wrote:
> On 16.11.2023 09:45, Nicola Vetrini wrote:
> > On 2023-11-15 12:22, Julien Grall wrote:
> >> But I noticed you were using gcc-12 and originally thought it was a 
> >> mistake until I saw the second use.
> >>
> >> The advantage of a variable CC (and CXX) is you can add a comment on 
> >> top why you are specifically requestion gcc-12? IOW, why is gcc not 
> >> fine?
> >>
> > 
> > The assumptions in C-language-toolchain.rst (which are reflected in the 
> > analysis config) are using gcc-12 explicitly; that's just easier from a 
> > certification perspective to have a fixed version.
> 
> I'm wondering: Upstream Xen isn't going to undergo any certification
> effort, aiui. Downstreams who want to do so may have good reasons to
> choose a specific compiler version, which may well not be gcc12. How
> are we meaning to deal with that?

I think the most important part is to detail all our dependencies on the
compiler and compiler's specific behaviors. If we do that, taking gcc12
as an example, then any downstream can look at C-language-toolchain.rst
and see if there are any differences or any gaps in their compiler of
choice compared to the reference (gcc12).

Re: [XEN PATCH v4 1/2] automation/eclair: make the docs for MISRA C:2012 Dir 4.1 visible to ECLAIR

[Julien Grall]

Hi,

On 16/11/2023 08:45, Nicola Vetrini wrote:
> On 2023-11-15 12:22, Julien Grall wrote:
>> Hi,
>>
>> On 15/11/2023 11:02, Nicola Vetrini wrote:
>>> On 2023-11-14 23:12, Julien Grall wrote:
>>>> Hi,
>>>>
>>>> On 14/11/2023 15:36, Nicola Vetrini wrote:
>>>>> To be able to check for the existence of the necessary subsections in
>>>>> the documentation for MISRA C:2012 Dir 4.1, ECLAIR needs to have a 
>>>>> source
>>>>> file that is built.
>>>>>
>>>>> This file is generated from 'C-runtime-failures.rst' in docs/misra
>>>>> and the configuration is updated accordingly.
>>>>>
>>>>> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
>>>>> ---
>>>>> Changes from RFC:
>>>>> - Dropped unused/useless code
>>>>> - Revised the sed command
>>>>> - Revised the clean target
>>>>>
>>>>> Changes in v2:
>>>>> - Added explanative comment to the makefile
>>>>> - printf instead of echo
>>>>>
>>>>> Changes in v3:
>>>>> - Terminate the generated file with a newline
>>>>> - Build it with -std=c99, so that the documentation
>>>>>    for D1.1 applies.
>>>>> Changes in v5:
>>>>> - Transform and build the file directly in the eclair-specific 
>>>>> directory
>>>>> ---
>>>>>   automation/eclair_analysis/build.sh   | 21 +++++++++++++++++++--
>>>>>   automation/eclair_analysis/prepare.sh |  7 ++++---
>>>>>   2 files changed, 23 insertions(+), 5 deletions(-)
>>>>>
>>>>> diff --git a/automation/eclair_analysis/build.sh 
>>>>> b/automation/eclair_analysis/build.sh
>>>>> index ec087dd822fa..f24292ed0643 100755
>>>>> --- a/automation/eclair_analysis/build.sh
>>>>> +++ b/automation/eclair_analysis/build.sh
>>>>> @@ -33,12 +33,29 @@ else
>>>>>     PROCESSORS=6
>>>>>   fi
>>>>>   +runtime_failures_docs() {
>>>>> +  doc="C-runtime-failures.rst"
>>>>> +  builddir="automation/eclair_analysis"
>>>>> +
>>>>> +  cp "docs/misra/${doc}" "${builddir}"
>>>>
>>>> Is it necessary to copy the .rst? IOW, would it be sufficient to use...
>>>>
>>>>> +  cd "${builddir}"
>>>>> +  printf "/*\n\n" >"${doc}.tmp"
>>>>> +  sed -e 's|\*/|*//*|g' "${doc}" >>"${doc}.tmp"
>>>>
>>>> ... docs/misc/${doc} here?
>>>>
>>>
>>> I didn't want to leave a stray file under docs/misra, but it's not 
>>> essential.
>>
>> I am confused. I am suggesting to use:
>>
>> sed -e 's|\*/|*//*|g' "../../docs/misc/${doc}" >> "${doc}.tmp"
>>
>> So *.tmp is still created at the same place.
>>
> 
> Ok, makes sense.
> 
>>>
>>>>> +  printf "\n\n*/\n" >>"${doc}.tmp"
>>>>> +  mv "${doc}.tmp" "${doc}.c"
>>>>
>>>> NIT: I am not sure why you need to first create .tmp and then create.c.
>>>>
>>>
>>> Wasn't this a pattern to defend against interruptions of the build, 
>>> just as I did in v3?
>>>
>>> +$(TARGETS:.o=.c): %.c: %.rst
>>> +    printf "/*\n\n" > $@.tmp
>>> +    sed -e 's|\*/|*//*|g' $< >> $@.tmp
>>> +    printf "\n\n*/\n" >> $@.tmp
>>> +    mv $@.tmp $@
>>
>> Yes but it makes sense for the Makefile because the target would not 
>> be re-executed if *.c exists.
>>
>> But I don't think this is the case for you because you are using a 
>> bash script. So your function should always be re-executed regardless 
>> on whether it was interrupted or not.
>>
> 
> Ok.
> 
>>>
>>>>> +
>>>>> +  # Cannot redirect to /dev/null because it would be excluded from 
>>>>> the analysis
>>>>> +  "${CROSS_COMPILE}gcc-12" -std=c99 -c "${doc}.c" -o "${doc}.o"
>>>>
>>>> NIT: It would be helpful to specify why -std=c99 is used. Above, you 
>>>> suggest this is to enable D1.1.
>>>>
>>>
>>> Yeah, the comment in the changelog should be pasted here
>>>
>>>> NIT: Can we define CC and use here and ...
>>>>
>>>>> +  cd -
>>>>> +}
>>>>> +
>>>>>   (
>>>>> -  cd xen
>>>>> +  runtime_failures_docs
>>>>>       make "-j${PROCESSORS}" "-l${PROCESSORS}.0"    \
>>>>>          "CROSS_COMPILE=${CROSS_COMPILE}"         \
>>>>>          "CC=${CROSS_COMPILE}gcc-12"              \
>>>>
>>>> ...? This would make easier to re-use the code.
>>>>
>>>
>>> I don't expect this build script to be changed much to be honest, but 
>>> if you think
>>> this is beneficial then it's ok.
>>
>> This is not only about code evolving. It makes easier to spot your are 
>> using the same compiler. I would not have made the remark if you were 
>> using 'gcc'.
>>
>> But I noticed you were using gcc-12 and originally thought it was a 
>> mistake until I saw the second use.
>>
>> The advantage of a variable CC (and CXX) is you can add a comment on 
>> top why you are specifically requestion gcc-12? IOW, why is gcc not fine?
>>
> 
> The assumptions in C-language-toolchain.rst (which are reflected in the 
> analysis config) are using gcc-12 explicitly; that's just easier from a 
> certification perspective to have a fixed version.

I am not against fixed version. It just needs to be documented. At least 
reading C-language-toolchain.rst, it is not obvious to me that this is 
only applying to GCC-12.

Cheers,

-- 
Julien Grall

Re: [XEN PATCH v4 1/2] automation/eclair: make the docs for MISRA C:2012 Dir 4.1 visible to ECLAIR

[Stefano Stabellini]

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

On Fri, 17 Nov 2023, Julien Grall wrote:
> Hi,
> 
> On 16/11/2023 08:45, Nicola Vetrini wrote:
> > On 2023-11-15 12:22, Julien Grall wrote:
> > > Hi,
> > > 
> > > On 15/11/2023 11:02, Nicola Vetrini wrote:
> > > > On 2023-11-14 23:12, Julien Grall wrote:
> > > > > Hi,
> > > > > 
> > > > > On 14/11/2023 15:36, Nicola Vetrini wrote:
> > > > > > To be able to check for the existence of the necessary subsections
> > > > > > in
> > > > > > the documentation for MISRA C:2012 Dir 4.1, ECLAIR needs to have a
> > > > > > source
> > > > > > file that is built.
> > > > > > 
> > > > > > This file is generated from 'C-runtime-failures.rst' in docs/misra
> > > > > > and the configuration is updated accordingly.
> > > > > > 
> > > > > > Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
> > > > > > ---
> > > > > > Changes from RFC:
> > > > > > - Dropped unused/useless code
> > > > > > - Revised the sed command
> > > > > > - Revised the clean target
> > > > > > 
> > > > > > Changes in v2:
> > > > > > - Added explanative comment to the makefile
> > > > > > - printf instead of echo
> > > > > > 
> > > > > > Changes in v3:
> > > > > > - Terminate the generated file with a newline
> > > > > > - Build it with -std=c99, so that the documentation
> > > > > >    for D1.1 applies.
> > > > > > Changes in v5:
> > > > > > - Transform and build the file directly in the eclair-specific
> > > > > > directory
> > > > > > ---
> > > > > >   automation/eclair_analysis/build.sh   | 21 +++++++++++++++++++--
> > > > > >   automation/eclair_analysis/prepare.sh |  7 ++++---
> > > > > >   2 files changed, 23 insertions(+), 5 deletions(-)
> > > > > > 
> > > > > > diff --git a/automation/eclair_analysis/build.sh
> > > > > > b/automation/eclair_analysis/build.sh
> > > > > > index ec087dd822fa..f24292ed0643 100755
> > > > > > --- a/automation/eclair_analysis/build.sh
> > > > > > +++ b/automation/eclair_analysis/build.sh
> > > > > > @@ -33,12 +33,29 @@ else
> > > > > >     PROCESSORS=6
> > > > > >   fi
> > > > > >   +runtime_failures_docs() {
> > > > > > +  doc="C-runtime-failures.rst"
> > > > > > +  builddir="automation/eclair_analysis"
> > > > > > +
> > > > > > +  cp "docs/misra/${doc}" "${builddir}"
> > > > > 
> > > > > Is it necessary to copy the .rst? IOW, would it be sufficient to
> > > > > use...
> > > > > 
> > > > > > +  cd "${builddir}"
> > > > > > +  printf "/*\n\n" >"${doc}.tmp"
> > > > > > +  sed -e 's|\*/|*//*|g' "${doc}" >>"${doc}.tmp"
> > > > > 
> > > > > ... docs/misc/${doc} here?
> > > > > 
> > > > 
> > > > I didn't want to leave a stray file under docs/misra, but it's not
> > > > essential.
> > > 
> > > I am confused. I am suggesting to use:
> > > 
> > > sed -e 's|\*/|*//*|g' "../../docs/misc/${doc}" >> "${doc}.tmp"
> > > 
> > > So *.tmp is still created at the same place.
> > > 
> > 
> > Ok, makes sense.
> > 
> > > > 
> > > > > > +  printf "\n\n*/\n" >>"${doc}.tmp"
> > > > > > +  mv "${doc}.tmp" "${doc}.c"
> > > > > 
> > > > > NIT: I am not sure why you need to first create .tmp and then
> > > > > create.c.
> > > > > 
> > > > 
> > > > Wasn't this a pattern to defend against interruptions of the build, just
> > > > as I did in v3?
> > > > 
> > > > +$(TARGETS:.o=.c): %.c: %.rst
> > > > +    printf "/*\n\n" > $@.tmp
> > > > +    sed -e 's|\*/|*//*|g' $< >> $@.tmp
> > > > +    printf "\n\n*/\n" >> $@.tmp
> > > > +    mv $@.tmp $@
> > > 
> > > Yes but it makes sense for the Makefile because the target would not be
> > > re-executed if *.c exists.
> > > 
> > > But I don't think this is the case for you because you are using a bash
> > > script. So your function should always be re-executed regardless on
> > > whether it was interrupted or not.
> > > 
> > 
> > Ok.
> > 
> > > > 
> > > > > > +
> > > > > > +  # Cannot redirect to /dev/null because it would be excluded from
> > > > > > the analysis
> > > > > > +  "${CROSS_COMPILE}gcc-12" -std=c99 -c "${doc}.c" -o "${doc}.o"
> > > > > 
> > > > > NIT: It would be helpful to specify why -std=c99 is used. Above, you
> > > > > suggest this is to enable D1.1.
> > > > > 
> > > > 
> > > > Yeah, the comment in the changelog should be pasted here
> > > > 
> > > > > NIT: Can we define CC and use here and ...
> > > > > 
> > > > > > +  cd -
> > > > > > +}
> > > > > > +
> > > > > >   (
> > > > > > -  cd xen
> > > > > > +  runtime_failures_docs
> > > > > >       make "-j${PROCESSORS}" "-l${PROCESSORS}.0"    \
> > > > > >          "CROSS_COMPILE=${CROSS_COMPILE}"         \
> > > > > >          "CC=${CROSS_COMPILE}gcc-12"              \
> > > > > 
> > > > > ...? This would make easier to re-use the code.
> > > > > 
> > > > 
> > > > I don't expect this build script to be changed much to be honest, but if
> > > > you think
> > > > this is beneficial then it's ok.
> > > 
> > > This is not only about code evolving. It makes easier to spot your are
> > > using the same compiler. I would not have made the remark if you were
> > > using 'gcc'.
> > > 
> > > But I noticed you were using gcc-12 and originally thought it was a
> > > mistake until I saw the second use.
> > > 
> > > The advantage of a variable CC (and CXX) is you can add a comment on top
> > > why you are specifically requestion gcc-12? IOW, why is gcc not fine?
> > > 
> > 
> > The assumptions in C-language-toolchain.rst (which are reflected in the
> > analysis config) are using gcc-12 explicitly; that's just easier from a
> > certification perspective to have a fixed version.
> 
> I am not against fixed version. It just needs to be documented. At least
> reading C-language-toolchain.rst, it is not obvious to me that this is only
> applying to GCC-12.

I did a commit sweep for the old MISRA patches. I didn't commit this
series as I imagine it requires a respin.

[XEN PATCH v4 2/2] docs/misra: add guidance on the format of Dir 4.1 docs for ECLAIR

[Nicola Vetrini]

Additional guidance on the formatting of the document for ECLAIR
is supplied.

Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>
---
 docs/misra/C-runtime-failures.rst | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/docs/misra/C-runtime-failures.rst b/docs/misra/C-runtime-failures.rst
index 1052b2afca13..cac51d6b2596 100644
--- a/docs/misra/C-runtime-failures.rst
+++ b/docs/misra/C-runtime-failures.rst
@@ -12,6 +12,14 @@ built-in checks that are present in the language.
 The presence of such documentation is requested by MISRA C:2012 Directive 4.1,
 whose headline states: "Run-time failures shall be minimized".
 
+The ECLAIR checker for MISRA C:2012 Directive 4.1 requires the documentation
+to be supplied using the following format:
+
+``Documentation for MISRA C:2012 Dir 4.1: <category> <description>``
+
+The matched categories are the ones listed below (e.g., ``overflow`` and
+``unexpected wrapping``). The content of the description is not checked and can
+span multiple lines.
 
 Documentation for MISRA C:2012 Dir 4.1: overflow
 ________________________________________________
-- 
2.34.1

Re: [XEN PATCH v4 2/2] docs/misra: add guidance on the format of Dir 4.1 docs for ECLAIR

[Stefano Stabellini]

On Tue, 14 Nov 2023, Nicola Vetrini wrote:
> Additional guidance on the formatting of the document for ECLAIR
> is supplied.
> 
> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>

Reviewed-by: Stefano Stabellini <sstabellini@kernel.org>

Re: [XEN PATCH v4 2/2] docs/misra: add guidance on the format of Dir 4.1 docs for ECLAIR

[Julien Grall]

Hi Nicola,

On 14/11/2023 15:36, Nicola Vetrini wrote:
> Additional guidance on the formatting of the document for ECLAIR
> is supplied.
> 
> Signed-off-by: Nicola Vetrini <nicola.vetrini@bugseng.com>

Acked-by: Julien Grall <jgrall@amazon.com>

Cheers,

-- 
Julien Grall